Blog
An Insight Into the AdaCore Ecosystem
Announcing Advent of Ada/SPARK 2025: Coding for a Cause!
Emmanuel Briot
Bookmarks in the GNAT Programming Studio (GPS)
As we improve existing views in GPS, we discover new ways to use them. This post shows some of the improvements done recently in the Bookmarks view,…
Claire Dross
Automatic Generation of Frame Conditions for Record Components
Formal verification tools like GNATprove rely on the user to provide loop invariants to describe the actions performed inside loops. Though the…
Yannick Moy
Research Corner - SPARK 2014 vs Frama-C vs Why3
Ready for a bloody comparison between technologies underlying the tools for SPARK 2014 vs Frama-C vs Why3? Nothing like that in that article we wrote…
Emma Adby
Introducing the Make With Ada competition!
Yannick Moy
Research Corner - Proving Security of Binary Programs with SPARK
Researchers from Dependable Computing and Zephyr Software LLC have presented at the latest NASA Formal Methods conference last week their work on…
Pierre-Marie de Rodat
C library bindings: GCC plugins to the rescue
Fabien Chouteau
Make with Ada: ARM Cortex-M CNC controller
Yannick Moy
GNATprove Tips and Tricks: Using the Lemma Library
A well-know result of computing theory is that the theory of arithmetic is undecidable. This has practical consequences in automatic proof of…
Claire Dross
Quantifying over Elements of a Container
Containers holding several items of the same type such as arrays, lists, or sets are a common occurrence in computer programs. Stating a property…
Florian Schanda
SPARKSMT - An SMTLIB Processing Tool Written in SPARK - Part I
Today I will write the first article in a short series about the development of an SMTLIB processing tool in SPARK. Instead of focusing on features,…
Emma Adby
Certification and Qualification
Jérôme Lambourg