[GAP] Announcing the immediate availability of the SPARK GPL Edition 2009

[Jamie Ayre]

Dear GAP members,

We are pleased to announce the release of SPARK GPL 2009,
the high-assurance software development Toolset for Academic
users and FLOSS developers. It includes the following features and
components:

- The SPARK Examiner for static analysis of SPARK programs
- The Simplifier automated theorem prover
- The Proof Checker interactive theorem prover
- The SPARKFormat tool for automatic reformatting of SPARK annotations
- The supporting tools, SPARKSimp, SPARKMake and POGS

SPARK GPL 2009 comes with version 4.3.1 of the GNAT Programming Studio
(GPS) IDE.

For a tutorial introduction to SPARK, illustrated using the Tokeneer
System developed by Praxis for the NSA, see the Tokeneer Discovery
Edition:

<http://www.adacore.com/home/products/sparkpro/tokeneer/discovery/>

The SPARK GPL Edition is available on Windows, SPARC/Solaris,
Linux (both 32- and 64-bit) and Mac OS X (64-bit).

SPARK GPL 2009 can be downloaded from the "Download" section on
GNAT Tracker:
<https://www.adacore.com/home/academia>