[GAP] SPARK GPL 2010-SMT Edition Now Available

[Jamie Ayre]

Dear GAP members,

We are pleased to announced the availability of the SPARK GPL 2010-SMT Edition. This release includes:

* SPARKBridge technology preview - SPARKBridge, a bridge between the SPARK tools and Satisfiable Modulo Theories (SMT) solvers, allows the use of alternate provers for automatically proving Verification Conditions. A linux-only preview, including the Alt-Ergo prover, is available as part of the GPL 2010-SMT release.

* New SPARK library packages, full-range array subtypes support, improved aliasing detection, and Verification Condition generation may now be specified on a file-by-file basis.

The SPARK GPL Edition is available on Linux (both 32- and 64-bit), Mac OS X, SPARC Solaris, and Windows. It is available from the "Download" section on GNAT Tracker.

You may also be interested to know that the first videos from the October 2010 High Assurance Software Symposium and SPARK User Group meeting are now available on-line:

http://www.adacore.com/home/ada_answers/lectures/spark_2010/