The AdaCore Blog
An Insight Into the AdaCore Ecosystem
SPARK Doesn't Comply With MISRA C. It Makes Most of It Moot.
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…
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…