SPARK 2014

Expanding the boundaries of safe and secure programming.

Learn more about SPARK 2014

Open Source

Common Research Lab Between AdaCore and INRIA

by Yannick Moy in Formal Verification, Open Source, News – January 10, 2014

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.

Muen Separation Kernel Written in SPARK

by Yannick Moy in Language, Formal Verification, Certification, Open Source, News – December 19, 2013

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.

GNATprove Takes the Train

by Yannick Moy in Language, Formal Verification, Open Source, News – April 11, 2013

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.

Axioms and Proofs: When Less is More

by Yannick Moy in Language, Open Source – February 15, 2013

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!

Future Version of SPARK Will Be Based on Ada 2012

by Yannick Moy in Language, Open Source, Events – November 30, 2012

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.