Blog
An Insight Into the AdaCore Ecosystem
Year in Review 2025: A Transformative Year for High-Integrity Software at AdaCore
Yannick Moy
Studies of Contracts in Practice
Two recent research papers focus on how program contracts are used in practice in open source projects, in three languages that support contracts…
Johannes Kanig
A Little Exercise With Strings
I recently looked at string manipulation functions in a library and tried to prove absence of run-time errors of one of them. Although the function…
Florian Schanda
Information Flo(w): Array Initialization in Loops
SPARK only supported array initialization using aggregates, as array initialization in loops raised a false alarm in flow analysis. Read on to learn…
Florian Schanda
SPARK 2014 Rationale: Data Dependencies
Programs often use a few global variables. Global variables make passing common information between different parts of a program easier. By reading…
Gem #157: Gprbuild and Code Generation
This series of Gems explains how gprbuild can be configured to invoke code generators before it compiles the resulting code itself.
Yannick Moy
GNATprove Tips and Tricks: How to Write Loop Invariants
Having already presented in previous posts why loop invariants are necessary for formal verification of programs with loops, and what loop invariants…
Gem #156: Listing Control in GNAT
Yannick Moy
Case Study for System to Software Integrity Includes SPARK 2014
My colleague Matteo Bordin will present at the upcoming Embedded Real Time Software and Systems conference in Toulouse in February a case study…
Claire Dross
SPARK 2014 Rationale: Verifying Properties over Formal Containers
We saw in a previous post how we could express complex properties over formal containers using quantified expressions. In this post, I present how…
Yannick Moy
Muen Separation Kernel Written in SPARK
The University of Applied Sciences Rapperswil in Switzerland has released last week an open-source separation kernel written in SPARK, which has been…
Claire Dross
SPARK 2014 Rationale: Expressing Properties over Formal Containers
We saw in a previous post how formal containers can be used in SPARK code. In this post, I describe how to express properties over the content of…