Blog
An Insight Into the AdaCore Ecosystem
Apr 16, 2026
Claire Dross
Formally Verified Hashed Sets in Ada SPARK
This blog explores the formal verification of an implementation of bounded hashed sets in Ada SPARK.
Read More
Mar 10, 2016
Yannick Moy
Formal Verification of Legacy Code
Mar 04, 2016
Yannick Moy
SPARK Prez at New Conference on Railway Systems
RSSR is a new conference focused on the development and verification of railway systems. We will present there how SPARK can be used to write…
Mar 03, 2016
Fabien Chouteau
Make with Ada: Candy dispenser, with a twist...
Mar 02, 2016
Emma Adby
Embedded Product Line Updates
Feb 23, 2016
Emma Adby
QGen 2.1 Release!
Jan 27, 2016
Emma Adby
Formal Verification Made Easy!
Jan 18, 2016
Emma Adby
ERTS and Embedded World conferences 2016
Jan 12, 2016
Jérôme Lambourg
Porting the Ada Runtime to a new ARM board
A step by step tutorial to adapt the ARM runtime to new MCUs/boards.
Dec 18, 2015
Yannick Moy, Emma Adby
Ada Lovelace Bicentennial
Dec 14, 2015
Emma Adby
Dissimilar tools: Use cases and impact on tool qualification level
Nov 30, 2015
Yannick Moy
GNATprove Tips and Tricks: What’s Provable for Real?
SPARK supports two ways of encoding reals in a program: the usual floating-point reals, following the standard IEEE 754, and the lesser known…
Nov 23, 2015
Yannick Moy
SPARK 2014 Rationale: Support for Ravenscar
As presented in a recent post by Pavlos, the upcoming release of SPARK Pro will support concurrency features of Ada, with the restrictions defined in…