SPARK 2014

Expanding the boundaries of safe and secure programming.

Learn more about SPARK 2014

Automatic Generation of Frame Conditions for Record Components

by Claire Dross in Formal Verification – July 26, 2016

Formal verification tools like GNATprove rely on the user to provide loop invariants to describe the actions performed inside loops. Though the preservation of variables which are not modified in the loop need not be mentioned in the invariant, it is in general necessary to state explicitly the preservation of unmodified object parts, such as record fields or array elements. These preservation properties form the loop’s frame condition. As it may seem obvious to the user, the frame condition is unfortunately often forgotten when writing a loop invariant, leading to unprovable checks. To alleviate this problem, the GNATprove tool now generates automatically frame conditions for preserved record components. In this post, we describe this new feature on an example.

Make with SPARK

by Yannick Moy in Events – June 20, 2016

AdaCore has launched the "Make with Ada" competition just today: teams of up to four have until September 30th to submit projects in Ada or SPARK which will be evaluated by a jury of four personalities of the embedded software domain: Bill Wong, Jack Ganssle, Dick Selwood and Cyrille Comar. The 5 prices range from a Crazyflie nano-copter to 5000 euros.

SPARK GPL 2016 Is Available

by Yannick Moy in News – June 1, 2016

The annual releases of GNAT GPL and SPARK GPL have just been announced, and can be downloaded from For SPARK, this means support of concurrency with Ravenscar, generation of counterexamples and better proof automation. Enjoy!

GNATprove Tips and Tricks: Using the Lemma Library

by Yannick Moy in Formal Verification – May 25, 2016

A well-know result of computing theory is that the theory of arithmetic is undecidable. This has practical consequences in automatic proof of programs which manipulate numbers. The provers that we use in SPARK have a good support for addition and subtraction, but much weaker support for multiplication and division. This means that as soon as the program has multiplications and divisions, it is likely that some checks won't be proved automatically. Until recently, the only way forward was either to complete the proof using an interactive prover (like Coq or Isabelle/HOL) or to justify manually the message about an unproved check. There is now a better way to prove automatically such checks, using the recent SPARK lemma library.

Quantifying over Elements of a Container

by Claire Dross in Formal Verification – May 17, 2016

Containers holding several items of the same type such as arrays, lists, or sets are a common occurrence in computer programs. Stating a property over such containers often involves quantifying over the elements they contain. The way quantified formulas over containers are translated for proof can be tuned in GNATprove using a specific annotation.

SPARKSMT - An SMTLIB processing tool written in SPARK - Part I

by Florian Schanda in Dev Projects, Formal Verification – April 21, 2016

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, I intend to focus on the how I have proved absence of run-time errors in the name table and lexer. I had two objectives: show absence of run-time errors, and do not write useless defensive code. Today's blog will be about the name table, a data structure found in many compilers that can map strings to a unique integer and back. The next blog post will talk about the lexical analyzer.