As automatic proof is time consuming, it is important that rework following a change in source code is minimized. GNATprove uses a combination of techniques to ensure that, both for a single user, and when working in a team.
The ProofInUse joint laboratory is currently improving the way SPARK deals with modular types and bitwise operators. Until now the SPARK tool was trying its best to translate those into equivalent operations on integers. It is now using native theory of smt-solvers when available resulting in much better support, and guaranteeing state of the art handling of bitwise operations. We present some examples in this post.
Users no longer have to provide a Refined_Global/Depends aspect when their Global/Depends mentions a state with visible refinement. Flow analysis now synthesizes and uses these aspects internally.
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.
GNATprove supports the suppression of warnings and justification of check messages with pragmas inserted in the source code. But these justifications may become obsolete across time. To help with that, GNATprove now issues a warning on useless justifications.
On Monday, we had a kickoff event for the ProofInUse joint lab between Inria and AdaCore. The slides of presentations are now available on the page of the event.
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!