Product Updates

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: