SPARK 2014

Expanding the boundaries of safe and secure programming.

Learn more about SPARK 2014

SPARK 2014 Rationale: Type Predicates

by Yannick Moy in Language, Formal Verification – July 24, 2015

Preconditions and postconditions define a very strong mechanism for specifying invariant properties over the program's control. What about similar properties for the program's data? It turns out Ada 2012 defined such a construct, type predicates, which was not supported in SPARK until now. And now it is.

Towards SPARK Pro 16.0 And Beyond…

by Yannick Moy in Events – July 9, 2015

The international team developing the SPARK product, usually dispersed across continents and islands (if UK still counts as an Island despite the Channel Tunnel), has gathered the last week of June to discuss the progress towards SPARK Pro 16.0, and beyond that. Here are the main points that we discussed.

Farewell Robert Dewar…

by Yannick Moy in News – July 4, 2015

It is with great sadness that I have to announce the death of Robert Dewar. Robert was President of AdaCore, and he has had a tremendous influence on the development of SPARK.

Constants in Contracts

by Pavlos Efstathopoulos in – June 26, 2015

Constants whose initial expressions depend on global variables or formal parameters can now appear in flow-related contracts. This allows more accurate specification and verification of information flow properties.

SPARK GPL 2015 Now Available

by Yannick Moy in News – June 18, 2015

The annual release of GNAT GPL and SPARK GPL have just been announced, and can be downloaded from libre.adacore.com. For SPARK, the changes are quite noticeable, with much improved provability, automation and usability. I know some people have been waiting for it for many months, so here it is!

SPARKSkein: From tour-de-force to run-of-the-mill Formal Verification

by Yannick Moy in Dev Projects, Formal Verification – June 1, 2015

In 2010, Rod Chapman released an implementation in SPARK of the Skein cryptographic hash algorithm, and he proved that this implementation was free of run-time errors. That was a substantial effort with the previous version of the SPARK technology. We have recently translated the code of SPARKSkein from SPARK 2005 to SPARK 2014, and used GNATprove to prove absence of run-time errors in the translated program. The difference between the two technologies is striking. The heroic effort that Rod put in the formal verification of the initial version of SPARKSkein could now be duplicated with modest effort and modest knowledge of the technology, thanks to the much greater proof automation that the SPARK 2014 technology provides, as well as various features that lower the need to provide supporting specifications, most notably contracts on internal subprograms and loop invariants.

How Our Compiler Learnt From Our Analyzers

by Yannick Moy in Compilation, Formal Verification – May 22, 2015

Program analyzers interpret the source code of a program to compute some information. Hopefully, the way they interpret the program is consistent with the way that the compiler interprets it to generate an executable, or the information computed is irrelevant, possibly misleading. For example, if the analyzer says that there are no possible run-time errors in a program, and you rely on this information to compile with dynamic checking off, it is crucial that no run-time error could occur as a result of a divergence of opinion between the analyzer and the compiler on the meaning of an instruction. We recently discovered such an inconsistency in how our compiler and analyzers dealt with floating-point exponentiation, which lead to a change in how GNAT now compile these operations.