Blog
An Insight Into the AdaCore Ecosystem
Year in Review 2025: A Transformative Year for High-Integrity Software at AdaCore
Fabien Chouteau
There's a mini-RTOS in my language
J. German Rivera
Make with Ada 2017- A "Swiss Army Knife" Watch
Yannick Moy, Martin Becker, Emanuel Regnath
Physical Units Pass the Generic Test
The support for physical units in programming languages is a long-standing issue, which very few languages have even attempted to solve. This issue…
Jonas Attertun
Make with Ada 2017: Brushless DC Motor Controller
This project involves the design of a software platform that provides a good basis when developing motor controllers for brushless DC motors…
Yannick Moy
Prove in the Cloud
We have put together a byte (8 bits) of examples of SPARK code on a server in the cloud. The benefit with this webpage is that anyone can now…
Yannick Moy
SPARK Tutorial at FDL Conference
Researcher Martin Becker is giving a SPARK tutorial next week at FDL conference. This post gives a link to his tutorial material (cookbook and…
Yannick Moy
New SPARK Cheat Sheet
Our good friend Martin Becker has produced a new cheat sheet for SPARK, that you may find useful for a quick reminder on syntax that you have not…
Pierre-Marie de Rodat
Highlighting Ada with Libadalang
Pierre-Marie de Rodat
Pretty-Printing Ada Containers with GDB Scripts
Yannick Moy
Proving Loops Without Loop Invariants
For all the power that comes with proof technology, one sometimes has to pay the price of writing a loop invariant. Along the years, we've strived to…
Yannick Moy
Research Corner - Focused Certification of SPARK in Coq
The SPARK toolset aims at giving guarantees to its users about the properties of the software analyzed, be it absence of runtime errors or more…
Yannick Moy
Applied Formal Logic: Searching in Strings
A friend pointed me to recent posts by Tommy M. McGuire, in which he describes how Frama-C can be used to functionally prove a brute force version of…