Blog
An Insight Into the AdaCore Ecosystem
Year in Review 2025: A Transformative Year for High-Integrity Software at AdaCore
Johannes Kanig
Explicit Assumptions in SPARK 2014
In this article, we provide a short introduction to our paper at the Test and Proof 2014 conference in York, UK.
Claire Dross
External Axiomatizations: a Trip Into SPARK’s Internals
There are cases expressing all the specification of a package in SPARK is either impossible (for example if you need to link them to elements of the…
Claire Dross
Manual Proof with Ghost Code in SPARK 2014
Guiding automatic solvers by adding intermediate assertions is a commonly used technique. We can go further in this direction, by adding complete…
Gem #160 : Developing unit tests with GNATtest
No one likes to spend the time on testing. It's tedious and boring writing the test harness, the tests themselves, and keeping them in sync with your…
Yannick Moy
Short Video Demo of SPARK 2014
New to SPARK? Want to "see" what's new in SPARK 2014? It's all in this 5 mn video demo!
Gem #159 : GPRinstall - Part 2
GPRinstall is a tool recently developed by AdaCore that provides an easy way to install a project, whether it be a standard project, a library…
Yannick Moy
Use of SPARK in a Certification Context
Using SPARK or any other formal method in a certification requires that the applicant agrees with the certification authority on the verification…
Gem #158: GPRinstall - Part 1
GPRinstall is a tool recently developed by AdaCore that provides an easy way to install a project, whether it be a standard project, a library…
Claire Dross
Contracts of Functions in SPARK 2014
In SPARK 2014, we can write a function F and annotate it with a pre and a postcondition. In this post, we explain how the SPARK 2014 proof tool…
Florian Schanda
SPARK 2014 Rationale: Information Flow
In a previous blog post we described how aspect Global can be used to designate the specific global variables that a subprogram has to read and…
Yannick Moy
Contextual Analysis of Subprograms Without Contracts
We have implemented a new feature in GNATprove for analyzing local subprograms in the context of their calls. This makes it possible to benefit from…
Johannes Kanig
Prove in Parallel with SPARK 2014
The article explains how we improved the performance of the SPARK 2014 toolset when multiple CPU cores are available for proof.