SPARK 2014

Expanding the boundaries of safe and secure programming.

Learn more about SPARK 2014

One Day Workshop Around SMT Solvers for ProofInUse Kickoff

by Yannick Moy in Events – December 15, 2014

To mark the start of the joint lab ProofInUse between Inria and AdaCore, whose purpose is to co-develop the SPARK and Why3 technologies, we will be hosting a one-day workshop around SMT solvers on Monday, February 2nd 2015, in the center of Paris. Registration if free but mandatory to attend the event.

A Gentle Introduction to SPARK

by Yannick Moy in Language, Formal Verification – December 11, 2014

As part of our work towards the releases of SPARK Pro 15.1 and SPARK GPL 2015 in a few months, we have rewritten completely the overview of the SPARK language in the SPARK User's Guide. We have also rewritten the section called GNATprove by Example that shows concrete examples of use of formal verification.

Using Coq to Verify SPARK 2014 Code

by Julien Thierry in Formal Verification – December 5, 2014

In the first release of SPARK 2014, GNATprove only provided support for automatic provers, in particular Alt-Ergo. Automatic provers are very handy when it comes to perform a big numberof simple proof. But they can fail to prove valid formulas when the proof involves some advanced reasoning. As mentioned in a previous post, one check left unproved might invalidate assumptions on which are based the proofs of multiple other checks. This is a case where manual proof may be useful for SPARK 2014 users. The development version of GNATprove now supports Coq to perform manual proof.

SPARK 16: Shipping CVC4, use two provers by default

by Johannes Kanig in Formal Verification – November 12, 2014

The SPARK toolset is shipped with prover CVC4 in addition to Alt-Ergo. We found that attempting proof first with CVC4, and if this fails, with Alt-Ergo, provides the best compromise between running time and proof result. Therefore, we decided to set this as the default behavior, which can be changed with option --prover.

SPARK Makes History

by Yannick Moy in Formal Verification, Events, Papers and Slides – October 29, 2014

Over its 20+ years of history, SPARK has known quite many cha(lle)nges. Rod Chapman, the "face" of SPARK for many years, wrote his account of this piece of history for a keynote presentation at ITP conference in July 2014. It's quite interesting to read after having just completed this year a major rewrite of the technology.

How to Write Subprogram Contracts

by Yannick Moy in Formal Verification, Design Method – September 30, 2014

GNATprove relies on subprogram contracts to be able to analyze subprograms independently from their callers and callees. But no contracts are compulsory: GNATprove can either generate a contract or use a default value when a contract is not provided by the user. Hence, it is important to know which contracts to write for which verification objectives.