Blog
An Insight Into the AdaCore Ecosystem
Formal Methods Practice and Theory
Raphaël Amiard
Make with Ada : From bits to music
Jack Mellor
2015: A Space Ada‑ssey
AdaCore has a long history of providing tools and support to develop mission critical applications for Space. Check out this video we made and showed…
Yannick Moy
SPARK 2014 Rationale: Type Predicates
Preconditions and postconditions define a very strong mechanism for specifying invariant properties over the program's control. What about similar…
Fabien Chouteau
Make with Ada: "The Eagle has landed"
July 20, 1969, 8:18 p.m. UTC, while a bunch of guys were about to turn blue on Earth, commander Neil A. Armstrong confirmed the landing of his Lunar…
Cyrille Comar
Farewell Robert...
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