Guiding automatic solvers by adding intermediate assertions is a commonly used technique. We can go further in this direction, by adding complete pieces of code doing nothing, generally called ghost code, to guide the automated reasoning. This is an advanced feature, for people willing to manually guide proofs. Still, it is all in SPARK 2014 and thus does not require the user to learn a new language. We explain here how we can achieve inductive proofs on a permutation function.
New to SPARK? Want to "see" what's new in SPARK 2014? It's all in this 5 mn video demo!
Time to release the GPL version of our new technology for SPARK based on the Why3 and Alt-Ergo technologies!
We will present SPARK at a couple of upcoming conferences in the USA and in Europe. Here are the dates to save in your calendar if you're interested.
Using SPARK or any other formal method in a certification requires that the applicant agrees with the certification authority on the verification objectives that this use of formal methods allows to reach, and how this is obtained and documented. In order to facilitate this process, the participants to the workshop on Theorem Proving in Certification have produced a draft set of guidelines, now publicly available.
In a previous blog post we described how aspect Global can be used to designate the specific global variables that a subprogram has to read and write. So, by reading the specification of a subprogram that has been annotated with aspect Global we can see exactly which variables, both local and global, are read and/or written each time the subprogram is called. Based purely on the Global aspect, this pretty much summarizes the full extent of our knowledge about the flow of information in a subprogram. To be more precise, at this point, we know NOTHING about the interplay between the inputs and outputs of the subprogram. For all we know, all outputs could be randomly generated and the inputs might not contribute in the calculation of any of the outputs. To improve this situation, SPARK 2014 uses aspect Depends to capture the dependencies between a subprogram's outputs and inputs. This blog post demonstrates through some examples how aspect Depends can be used to facilitate correct flow of information through a subprogram.
In SPARK 2014, we can write a function F and annotate it with a pre and a postcondition. In this post, we explain how the SPARK 2014 proof tool handles a call to such a function.
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!