SPARK Pro 9.0
AdaCore is pleased to announce the availability of SPARK Pro 9 available on the following platforms:
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: