SPARK 2014

Expanding the boundaries of safe and secure programming.

Learn more about SPARK 2014

SPARK 16: Generating Counterexamples for Failed Proofs

by in Formal Verification – November 3, 2015

While the analysis of failed proofs is one of the most challenging aspects of formal verification, it would be much easier if a tool would automatically find values of variables showing why a proof fails. SPARK Pro 16, to be released in 2016, is going to introduce such a feature. If a proof fails, it attempts to generate a counterexample exhibiting the problem. This post introduces this new feature, developed in the scope of the ProofInUse laboratory.

GNATprove Tips and Tricks: User Profiles

by Yannick Moy in Formal Verification – October 20, 2015

One of the most difficult tasks when using proof techniques is to interact with provers, in particular to progressively increase proof power until everything that should be proved is proved. Until the last release, increasing the proof power meant operating on three separate switches. There is now a simpler solution based on a new switch --level, together with a simpler proof panel in GPS for new users.

SPARK 2014 Rationale: Variables That Are Constant

by in Language, Formal Verification – September 22, 2015

The SPARK tools now support yet another feature that allows users to better specify the intended behavior of their programs. This new feature enables users to declare that specific variables can only be updated during the elaboration of their enclosing package. Read on if you want to know more...

The Eight Reasons For Using SPARK

by Yannick Moy in Formal Verification, Design Method, Certification, Papers and Slides – September 21, 2015

Based on our many years of experience with our customers using SPARK in their projects, we have come up with a list of eight objectives that are most commonly targeted when using SPARK. Most projects only target a few of them, but in theory one could try to achieve all of them with SPARK on a project. This list may be useful for those who want to assess if the SPARK technology can be of benefit in their context, and to existing SPARK users to compare their existing practice with what others do.

Book on SPARK 2014 Is Available

by Yannick Moy in Formal Verification, News – September 18, 2015

I am very pleased to announce that a book is now available for those who want to learn formal verification with SPARK 2014. This book was written by Prof. John McCormick from University of Northern Iowa and Prof. Peter Chapin from Vermont Technical College. We've been interacting a lot with them since they started in 2013, and the result of these interactions is quite satisfying!

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.