SPARK Pro 9.0 – March 22, 2010

AdaCore is pleased to announce the availability of SPARK Pro 9 available on the following platforms:

sparc-solaris
x86-linux
x86_64-darwin
x86_64-linux
x86-windows

This is a major release including many new features:

• New information-flow verification for safety and security policies, such as Bell-LaPadula, based on integrity labeling of own variables.
• New SPARK2005 language profile is now available. At present, basic Ada2005 features supported include ‘Mod, ‘Machine_Rounding, new reserved words, and the static semantics of “overriding”.
• New ZombieScope tool that detects dead statements, branches and paths in SPARK code, complementing the capabilities of the Simplifier and POGS.
• Cross Referencing annotations in GPS.
• Function return annotations are now treated more like procedure post-conditions, being substituted into the VC hypotheses of the caller thus dramatically improving the effectiveness of the theorem prover.
• A new output format for POGS designed to be both easier to read and easier to search automatically. It also reflects the results of the new ZombieScope tool.
• Case checking. New Examiner switch that insists on consistent casing within annotations.

The new features will be presented in a webinar on April 27. For more information and to register, please visit:

http://www.adacore.com/home/products/gnatpro/webinars