Blog
An Insight Into the AdaCore Ecosystem
Formal Methods Practice and Theory
Fabien Chouteau
RecordFlux State Machines
In a previous post we presented the RecordFlux specification language and toolset, illustrating how to design and generate formally proven binary…
Nicolas Setton
Reducing Ada code bases with adareducer
How we're using Libadalang to create an automated Ada code reducer.
Yannick Moy
Explainable Program Proofs
Ever wanted to understand why program proof is not as easy as telling ChatGPT "can you prove that program <code>stuff</code> is correct for me?" A…
Yannick Moy
The Case for SPARK Evolution - an April First Parable
SPARK already allows you to specify functional contracts by cases, and soon it will allow you to specify cases that lead to an exception. But what…
Fabien Chouteau
The End of Binary Protocol Parser Vulnerabilities
This week we announced a new tool called RecordFlux. The goal of RecordFlux is to address one of the most critical parts of the software stack in…
Maxim Reznik
Introduction to VSS library
The VSS (as an abbreviation for Virtual String Subsystem) library is designed to provide advanced string and text processing…
Fabien Chouteau
GNAT Pro 21.6 for LYNX MOSA.ic for Avionics (MfA)
Paul Butcher
Automated Assurance through Differential Fuzzing
This blog describes the concept and benefits of differential fuzz testing. In addition, the post describes setting up, executing and analyzing the…
Fabien Chouteau
AdaCore joins the Rust foundation
Last year we announced our strategic partnership with Ferrous Systems, a technology company specializing in the Rust programming language. Today we…
Fabien Chouteau
AdaCore at FOSDEM 2023
Fabien Chouteau
Ada/SPARK Crate Of The Year 2022 Winners Announced!
Fabien Chouteau
Advent of Ada/SPARK 2022 Results
At the end of November we called the Ada and SPARK programmers community to take on a challenge for a good cause. We are now in January and it is…