SPARK GPL Edition
2011 GPL Edition Now Available!
SPARK GPL provides the foremost language, toolset and design discipline for the engineering of high-assurance software. It combines the renowned SPARK language and verification tools from Altran Praxis with the GNAT Programming Studio (GPS) and GNATBench development environments from AdaCore.
This release includes:
- 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 2011 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.
The SPARK GPL Edition is available on Linux (both 32- and 64-bit), Mac OS X (64-bit), Windows.
AdaCore and Praxis 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.
The SPARK GPL Edition consists of the following technologies:
View the SPARK Comparison Chart
Learn more about the commercially supported version of SPARK – SPARK Pro
