Blog
An Insight Into the AdaCore Ecosystem
Mar 19, 2026
Kyriakos Georgiou
Hardware-Driven Security: Can CHERI Fix the "Blind Spots" of Software Testing?
This work combines fuzz testing with CHERI hardware. Unlike heuristic-based sanitizers, CHERI uses hardware-enforced capabilities - pointers with…
Read More
Jul 15, 2013
Yannick Moy
SPARK 2014 Rationale: Specification Functions
Specifying a program's behavior is seldom expressible in a satisfiable way without the capability of abstraction provided by function calls. Yet,…
Jul 07, 2013
Yannick Moy
SPARK 2014 Rationale: Contract Cases
Besides the usual expression of a subprogram contract as a pair of a precondition and a postcondition, SPARK 2014 provides a way to express such a…
Jul 07, 2013
Johannes Kanig
SPARK 2014 goes to Space!
David Lesens from Astrium was a member of the Hi-Lite project ("was" because the project is finished now, see the previous post), and has tried…
Jul 01, 2013
Gem #151 : Specifying Mathematical Properties of Programs
Jun 17, 2013
Gem #150: Out and Uninitialized
Jun 03, 2013
Gem #149 : Asserting the truth, but (possibly) not the whole truth
Jun 02, 2013
Yannick Moy
Project Hi-Lite Wrap-up
After three years of hard work, we have reached last week the end of project Hi-Lite, whose goal was to simplify the use of formal methods. We're…
May 20, 2013
Gem #148 : Su(per)btypes in Ada 2012 - Part 3
May 06, 2013
Gem #147 : Su(per)btypes in Ada 2012 - Part 2
Apr 22, 2013
Gem #146 : Su(per)btypes in Ada 2012 - Part 1
Apr 08, 2013
Gem #145: Ada Quiz 3 - Statements
Mar 25, 2013