SPARK Pro 21.x

Watch this video to see a summary of SPARK Pro 21.x roadmap >>

See the full SPARK Pro 21 release notes >>

SPARK Pro 20.x

  • Support for pointers through ownership
  • Support for volatile variables to prevent compiler optimizations
  • Contracts added to Ada Standard Library
  • Improved floating-point support in Alt-Ergo prover
  • Better support for recursive functions
  • Parallel analysis of subprograms
  • Better messages from flow analysis
  • Dead code detected by proof warnings
  • Unproved parts of preconditions identified
  • Automatic target configuration for GNAT runtimes
  • Ability to specify file-specific switches

See the full SPARK 20 Release notes »

SPARK Pro 19.x

  • Support for more fixed-point types and operations
  • New lemmas for exponentiation, fixed-point arithmetic and higher-order functions
  • Automatic detection of array initialization with non-static bounds
  • Improved support for floating-point computations
  • Explanation part in messages to investigate unproved checks
  • Warnings issued by proof to detect inconsistencies
  • Counterexamples on individual paths through subprograms
  • Possibility to run analysis on region of code in GPS
  • New Analysis Report panel in GPS
  • Speedup on large projects

See the full SPARK 19 Release notes »

SPARK Pro 18.x

  • Easier program specification
    • Preconditions on standard numerical functions
    • Contracts on formal containers
    • Specification of subprogram termination
  • Greater proof automation
    • Better integration of CodePeer engine as additional prover
    • Unrolling of simple for-loops
    • Enhanced library of lemmas for floating-point arithmetic
  • Ability to perform interactive proof in GPS
  • Easier tool configuration with cross runtimes
  • Support for caching using memcached

See the full SPARK 18 Release notes »

SPARK Pro 17.x

  • Improved proof automation
    • CodePeer engine available as an additional prover
    • Generation of loop invariants for frame conditions
    • Library of lemmas for non-linear arithmetic
    • Finer granularity in proof of conjunctions
  • Improved proof interaction
    • Improved counterexamples (arrays, quantifiers, enumerations)
    • New mode statistics for proof results
    • Display mode for proof
    •  Replay mode for proof
  • Support for type invariants

See the full SPARK 17 Release notes »