Blog
An Insight Into the AdaCore Ecosystem
AdaCore Software Supply Chain Security Evolution
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…
Yannick Moy
(Many) More Low Hanging Bugs
We reported in a previous post our initial experiments to create lightweight checkers for Ada source code, based on the new Libadalang technology.…
Yannick Moy, Emmanuel Briot, Nicolas Roche
A Usable Copy-Paste Detector in A Few Lines of Python
After we created lightweight checkers based on the recent Libadalang technology developed at AdaCore, a colleague gave us the challenge of creating a…
Yannick Moy
VerifyThis Challenge in SPARK
This year again, the VerifyThis competition took place as part of ETAPS conferences. This is the occasion for builders and users of formal program…
Anthony Leonardo Gracio
GPS for bare-metal developers
Emmanuel Briot
User-friendly strings API
Yannick Moy
GNATprove Tips and Tricks: Proving the Ghost Common Divisor (GCD)
Euclid's algorithm for computing the greatest common divisor of two numbers is one of the first ones we learn in school, and also one of the first…
Emmanuel Briot
New strings package in GNATCOLL
This post describes the new GNATCOLL.Strings package, and the various optimizations it performs to provide improved performance.