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.
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.
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.
A recent blog post describes in details how SPARK can be used to program a basic Tetris program for the ARM Cortex M4. For formal verification hackers and embedded platforms hackers alike!
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.
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.
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.
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.
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.
Ensuring that all variables, both the visible ones and the ones exposed through state abstractions, are initialized is not a trivial task. SPARK 2015 helps users get their design right by issuing a warning for every state abstraction that is impossible to initialize. This blog post explains how this new feature works.