We are pleased to announce the release of SPARK GPL 2011, the foremost language, toolset and design discipline for the engineering of high-assurance software. SPARK GPL is the version dedicated to the academic and Free Software communities. This latest edition provides many new features and enhancements in all areas of the technology. The most notable ones are:
– 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.
SPARK GPL 2011 comes with version 5.0.1 of the GNAT Programming Studio IDE and GNATbench 2.5.1, the GNAT plug-in for Eclipse.
The SPARK GPL Edition is available on Windows, SPARC/Solaris, Linux (both 32- and 64-bit) and Apple’s OS X (64-bit).
SPARK GPL 2011 can be downloaded from the “Download” section on https://libre.adacore.com.
