SPARK 2014

Expanding the boundaries of safe and secure programming.

Learn more about SPARK 2014

GNATprove Tips and Tricks: Catching Mistakes in Contracts

by Yannick Moy in Formal Verification – February 18, 2015

Contracts may be quite complex, as complex as code in fact, so it is not surprising that they contain errors sometimes. GNATprove can help by pinpointing suspicious constructs that, although legal, do not make much sense. These constructs are likely to be caused by mistakes made by the programmer when writing the contract. In this post, I show examples of incorrect constructs that are signaled by GNATprove.

The Kickoff Meeting of the SOPRANO project

by Johannes Kanig in Formal Verification, Events – January 23, 2015

The SOPRANO project is a research project funded by the ANR (French National Research Agency) whose aim is to improve automatic proof in specific problem domains where current automatic provers are weak or have blind spots. If successful, the project will result in more proved VCs in the SPARK toolset, better counterexamples and overall easier handling of the tools. The Kickoff Meeting of SOPRANO was held on Wednesday, Jan 15th 2015, at the CEA NanoInnov building.

SPARK 2014 Rationale: Functional Update

by Yannick Moy in Language, Formal Verification – January 21, 2015

While attribute Old allows expressing inside postconditions the value of objects at subprogram entry, this is in general not enough to conveniently express how record and array objects are modified by a procedure. A special attribute Update is defined in SPARK to make it easy to express such properties.

SPARK 2014 Rationale: Object Oriented Programming

by Yannick Moy in Language, Formal Verification – January 14, 2015

Object Oriented Programming is known for making it particularly difficult to analyze programs, because the subprograms called are not always known statically. The standard for civil avionics certification has recognized this specific problem, and defines a specific verification objective called Local Type Consistency that should be met with one of three strategies. SPARK allows using one of these strategies, by defining the behavior of an overridden subprogram using a special class-wide contract and checking that the behavior of the overriding subprogram is a suitable substitution, following the Liskov Substitution Principle.

SPARK 2014 Rationale: Ghost Code

by Yannick Moy in Language, Formal Verification – January 7, 2015

A common situation when proving properties about a program is that you end up writing additional code whose only purpose is to help proving the original program. If you're careful or lucky enough, the additional code you write will not impact the program being verified, and it will be removed during compilation, so that it does not inflate binary size or waste execution cycles. SPARK provides a way to get these benefits automatically, by marking the corresponding code as ghost code, using the new Ghost aspect.

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.