Product Updates

SPARK Pro 17

- 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