The repository on the open-do forge is now obsolete. SPARK2014 and its components Why3, Alt-Ergo, CVC4 and Z3 are available on github.
Floating point problems are difficult and interesting. This blog post describes the process of creating floating point benchmarks: one of the activities are doing to help out the SMTLIB effort (SMTLIB is the language our VCs are expressed in).
The upcoming releases SPARK Pro 14 and SPARK GPL 2014 will be based on the Why3 technology developed by the French research laboratory INRIA. It took us four years, as part of project Hi-Lite, to switch from the older technology to this new one. We are now planning for a closer relationship with INRIA to further evolve this technology, through a common research laboratory that will start operating in October 2014.
The University of Applied Sciences Rapperswil in Switzerland has released last week an open-source separation kernel written in SPARK, which has been proved free from run-time errors. This project is part of the secure multilevel workstation project by Secunet, a German security company, which is using SPARK and Isabelle to create the next generation of secure workstations providing different levels of security to government employees and military personnel. I present why I think this project is worth following closely.
Yesterday, I attended the PhD thesis Defence of Mohamed Iguernelala at the lab of the research team Toccata at INRIA, France. Mohamed has done a lot of work on the SMT prover Alt-Ergo which is used in SPARK 2014.
AdaCore and Altran have published today the new version of SPARK GPL, for SPARK 2014. Here is a link to the download page.
David Mentré from Mitsubishi Electric R&D Centre Europe has produced a very interesting report on his use of GNATprove (the formal verification tool we develop for the next version of SPARK) on a case-study from the Open-ETCS European project, to develop the tools for the future European Train Control Systems.
In formal verification, we ultimately rely on automatic provers to decide whether formulas are valid (always true) or not. In GNATprove for example, we rely mostly on the ability of prover Alt-Ergo to analyze quickly the formulas we generate, and answer yes when the formula is valid or no when the formula is invalid (so there is a problem with the code or the assertions in the program). The reality is that the prover may take a long time to reply yes/no, and that in some cases it just replies I don’t know!
At the SPARK User Day yesterday in Bath, Altran-Praxis and AdaCore announced that the SPARK language will undergo a major transformation, to both extend the subset of Ada included in SPARK, and to use the new specification features of Ada 2012 instead of special comments like in today’s SPARK language.
This is the paper that Yannick Moy presented at the recent ERTS 2012 conference: Verification activities mandated for critical software are essential to achieve the required level of confidence expected in life-critical or business-critical software.