We have implemented a new feature in GNATprove for analyzing local subprograms in the context of their calls. This makes it possible to benefit from the most precise analysis for local subprograms, without incurring the cost of adding contracts to these subprograms.
The article explains how we improved the performance of the SPARK 2014 toolset when multiple CPU cores are available for proof.
The commercial version of the new SPARK tools, SPARK Pro 14.0, is released today for AdaCore and Altran customers. This is the first official release of this new technology based on the Why3 and Alt-Ergo technologies. A non-commercial GPL licensed version for academics will be released next month. We're happy to show you the results of four years of work!
Two recent research papers focus on how program contracts are used in practice in open source projects, in three languages that support contracts (Eiffel obviously, Java with JML contracts and C# with Code Contracts). I'm reporting what I found interesting (and less so) in these two studies.
The ease of use of the new SPARK technology lies for a large part in the much improved proof automation provided by the use of a state-of-the-art SMT solver at the heart of our technology. If you're interested in this subject, you may want to attend to one of two talks which take place in Saclay near Paris next week.
I recently looked at string manipulation functions in a library and tried to prove absence of run-time errors of one of them. Although the function and it's proof are quite simple in the end, the process of obtaining the correct code and the proof was interesting enough to write this blog post.
SPARK only supported array initialization using aggregates, as array initialization in loops raised a false alarm in flow analysis. Read on to learn how the situation has been improved in SPARK 2014.
Programs often use a few global variables. Global variables make passing common information between different parts of a program easier. By reading the specification of a subprogram we are able to see all of the parameters that the subprogram uses and, in Ada, we also get to know whether they are read, written or both. However, no information regarding the use of global variables is revealed by reading the specifications. In order to monitor and enforce which global variables a subprogram is allowed to use, SPARK 2014 has introduced the Global aspect, which I describe in this post.
Having already presented in previous posts why loop invariants are necessary for formal verification of programs with loops, and what loop invariants are necessary for various loops, we detail here a methodology for how users can come up with the right loop invariants for their loops. This methodology in four steps allows users to progressively add the necessary information in their loop invariants, with the tool GNATprove providing the required feedback at each step on whether the information provided is sufficient or not.
My colleague Matteo Bordin will present at the upcoming Embedded Real Time Software and Systems conference in Toulouse in February a case study showing how formal verification with SPARK can be included in a larger process to show preservation of properties from the system level down to the software level. The case study is based on the Nose Gear challenge from the Workshop on Theorem Proving in Certification.