share article

Share on facebook
Share on twitter
Share on linkedin

AdaCore and Altran Praxis Release SPARK Pro 11


Increased verification efficiency for high-assurance systems

High Assurance Software Symposium and SPARK User Group – AdaCore and Altran Praxis today announced the release of the SPARK Pro 11 software development and verification environment, providing a major step forward for the developers of high-assurance systems. SPARK Pro 11 offers many enhancements particularly in the area of program proof.

Major improvements to proof functions

A number of significant enhancements have been made to the way that functions and proof functions are handled in SPARK Pro 11. These changes will improve project efficiency by eliminating the vast majority of rules that were previously manually encoded. The main changes include a more powerful language for specifying proof functions and the ability to use the functions in any proof context. This greatly simplifies the task of writing and maintaining functional contracts for critical software, providing high-assurance at lower cost.

Counter-example generation

Proof is a very powerful technique for achieving high levels of assurance in safety or security-critical software. However, when performing proofs users typically spend much of their time inspecting undischarged “verification conditions” to determine whether they can indeed be proved. Included with SPARK Pro 11, Riposte is a new tool that not only determines whether a verification condition is false, but can also generate a counter-example to demonstrate the conditions under which it is false. Riposte is a major improvement to the verification workflow, saving projects a significant amount of time previously spent analysing improvable verification conditions and providing developers with intuitive explanations. Riposte was developed jointly by Altran Praxis and the University of Bath (UK).

Clearly defined assumptions

The new assume contract in SPARK Pro 11 allows users to introduce system-level assumptions about programs into their proofs in a clear and concise format. Previously, these assumptions might have been captured by user rules or manual review.

Tel. +33 1 49 70 67 16

Share this article

Share on facebook
Share on twitter
Share on linkedin

Related Posts

View Latest Magazine

Subscribe today

Member Login