Product Updates

SPARK Pro 10

AdaCore is pleased to announce the availability of SPARK Pro 10 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:

Automatic selection of flow analysis mode
The Examiner now supports automatic selection of information flow or data flow analysis on a per subprogram basis.

KCG Language Profile
As part of a collaborative development with Esterel Technologies, a new language profile has been added to the Examiner for processing automatically-generated SPARK code produced by Esterel's KCG code generator for SCADE.

Derived Numeric Types
Definition of numeric types has been made easier in Release 10.0 by the introduction of language and tool support for explicitly derived numeric types.

SPARKBridge preview for Windows
SPARKBridge - a bridge between the SPARK tools and Satisfiable Modulo Theories (SMT) solvers - is now available as a preview to Windows users, allowing them to trial alternate provers for discharging Verification Conditions.

Library Additions
The SPARK library has been augmented with several new packages including:

  • Interfaces
  • Ada.Characters.Handling
  • Ada.Text_IO

Improvements to Proof Tools
The Simplifier now has enhanced reasoning capabilities for modular types, allowing more proofs to be automatically discharged. In addition, the proof summary output (from the POGS tool) has been improved to make the management of the proof process easier for large projects.

The new features will be presented in a webinar on July 5. For more information and to register, please visit:
www.adacore.com/home/products/sparkpro/language_toolsuite/webinars