Blog

Pat Rogers

From Ada to Platinum SPARK: A Case Study for Reusable Bounded Stacks

This blog entry describes the transformation of an Ada stack ADT into a completely proven SPARK implementation that relies on static verification…

Abe Cohen

An Introduction to Contract-Based Programming in Ada

Johannes Kliemann

Ada on the ESP8266

Not long ago, AdaCore published its LLVM frontend for GNAT. Also quite recently Espressif updated their LLVM backend to LLVM 9 which also happens to…

Martyn Pike

A Trivial File Transfer Protocol Server written in Ada

For an upcoming project, I needed a simple way of transferring binary files over an Ethernet connection with minimal (if any at all) user…

Roderick Chapman

Proving properties of constant-time crypto code in SPARKNaCl

Over the last few months, I developed a SPARK version of the TweetNaCl cryptographic library. This was made public on GitHub in February 2020, under…

Ghjuvan Lacambre

Time travel debugging in GNAT Studio with GDB and RR

Learn how to use GDB and RR's advanced time traveling features in GNAT Studio.

Maxim Reznik

Android application with Ada and WebAssembly

Pat Rogers

Making an RC Car with Ada and SPARK

Pierre-Marie de Rodat

A Further Expedition into Libadalang: Save Time with Libadalang.Helpers.App

Vadim Godunko

Using GNAT-LLVM to target Ada to WebAssembly

Fabien Chouteau

AdaCore at FOSDEM 2020

Fabien Chouteau

Ada on a Feather

I was quite happy to see AdaFruit release their first Feather format board including a micro-controller with plenty of Ada support, the STM32F4. I…