Blog
An Insight Into the AdaCore Ecosystem
Formally Verified Hashed Sets in Ada SPARK
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…
Rob Tice
The Adaroombot Project
The Adaroombot project consists of an iRobot CreateⓇ 2 and Ada running on a Raspberry Pi with a Linux OS. This is a great Intro-to-Ada project as it…
Pierre-Marie de Rodat, Nicolas Setton
GNAT GPL 2017 is out!
Fabien Chouteau
Ada on the first RISC-V microcontroller
Yannick Moy
Research Corner - FLOSS Glider Software in SPARK
Two years ago, we redeveloped the code of a small quadcopter called Crazyflie in SPARK, as a proof-of-concept to show it was possible to prove…
Yannick Moy
Research Corner - Floating-Point Computations in SPARK
It is notoriously hard to prove properties of floating-point computations, including the simpler bounding properties that state safe bounds on the…
Yannick Moy
Frama-C & SPARK Day Slides and Highlights
The Frama-C & SPARK Day this week was a very successful event gathering the people interested in formal program verification for C programs (with…