Blog
An Insight Into the AdaCore Ecosystem
MISRA for Memory Safety
Fabien Chouteau
Make with Ada: All that is useless is essential
A few weeks ago I discovered the wonderful world of solenoid engines. The idea is simple: take a piston engine and replace explosion with…
Yannick Moy
SPARKSkein: From tour-de-force to run-of-the-mill Formal Verification
In 2010, Rod Chapman released an implementation in SPARK of the Skein cryptographic hash algorithm, and he proved that this implementation was free…
Anthony Leonardo Gracio
How to prevent drone crashes using SPARK
The Crazyflie is a very small quadcopter sold as an open source development platform: both electronic schematics and source code are directly…
Yannick Moy
How Our Compiler Learnt From Our Analyzers
Program analyzers interpret the source code of a program to compute some information. Hopefully, the way they interpret the program is consistent…
Emmanuel Briot
Count them all (reference counting)
Emmanuel Briot
Larger than it looks (storage pools)
This post shows how to implement a special storage pool that allocates an extra header every time it allocates some memory. This can be used to store…
Karen Mason
What's in the Box?
Emma Adby
Project P Open Workshop
Emma Adby
Verification on Ada code with Static and Dynamic Code Analysis - Webinar
Karen Mason
The Year for #AdaLove
Claire Dross
A quick glimpse at the translation of Ada integer types in GNATprove
In SPARK, as in most programming languages, there are a bunch of bounded integer types. On the other hand, Why3 only has mathematical integers and a…
Martyn Pike