Blog

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…

Yannick Moy

New Guidance for Adoption of SPARK

While SPARK has been used for years in companies like Altran UK, companies without the same know-how may find it intimidating to get started on…

Fabien Chouteau

DIY Coffee Alarm Clock

A few weeks ago one of my colleagues shared this kickstarter project : The Barisieur. It’s an alarm clock coffee maker, promising to wake you up with…