SPARK GPL Edition
2015 GPL Edition Now Available!
SPARK GPL 2015 - the formal method verification toolset - includes a number of major enhancements. New language features include in particular support for Object-Oriented programming and "ghost code" used for proof only, with no impact on the generated code.
Proof capability has been significantly improved with the integration of two provers by default (Alt-Ergo and CVC4), additional automatic generation of contracts, more precise analysis of modular (bitwise) operations, and improved support for manual provers.
Usability has also been enhanced through better categorization of messages and output of assumptions made for each verification result.
You will find documentation about the SPARK 2014 toolset here:
See in particular the SPARK 2014 Toolset User's Guide to get started. You can also read more about the SPARK 2014 language - including a growing number of tips and tricks here: http://www.spark-2014.org
AdaCore and Altran are dedicated to developing the finest tools available for software development with SPARK and Ada. The SPARK GPL Edition is the development environment for Free Software development and the GNAT Academic Program for use in Academia. SPARK Pro is for commercial/industrial development.
- Automatic selection of flow analysis mode – the Examiner now supports automatic selection of information flow or data flow analysis on a per subprogram basis.
- Derived Numeric Types – definition of numeric types has been made easier in GPL 2012 by the introduction of language and tool support for explicitly derived numeric types.
- SPARKBridge preview for Windows – SPARKBridge, a bridge between the SPARK tools and Satisfiable Modulo Theories (SMT) solvers – is now available as a preview to Windows users, allowing them to trial alternate provers for discharging Verification Conditions.
- Library Additions – the SPARK library has been augmented with several new packages including: Interfaces, Ada.Characters.Handling, Ada.Text_IO
Improvements to Proof Tools - the Simplifier now has enhanced reasoning capabilities for modular types, allowing more proofs to be automatically discharged. In addition, the proof summary output (from the POGS tool) has been improved to make the management of the proof process easier for large projects.
- The SPARK Language Definition
- Full SPARK Toolset, including Examiner, Simplifier and Checker
- Supporting SPARK tools: SPARKSimp, SPARKMake, SPARKFormat and POGS, ViCToR Wrapper, and ZombieScope
- Tutorial material for SPARK GPL and SPARK Pro are included in the accompanying release of the Tokeneer Discovery package.