Abstract

SPARK is a subset of Ada used primarily in high-integrity systems in the aerospace, defence, rail and security industries. In this talk we compare a prover from Praxis UK, the Simplify prover used in the ESC /Java static program verifier, and the SMT (SAT Modulo Theories) solvers Yices and CVC3 .

We observe that Praxis’s prover can prove more VCs than the other provers because it can handle some relatively simple non-linear problems, though, by adding some axioms about division and modulo operators to the other provers, the gap can be narrowed. One advantage of the other provers is their ability to produce counter-example witnesses to VCs that are not valid.

The work is the first step in a wider project to increase the fraction of VCs from current SPARK programs that can be proved automatically and to broaden the range of properties that can be automatically checked. Project interests include improving support for non-linear arithmetic and for automatic loop invariant generation.

This work builds on previous work by Kathleen Sharp and Bill Ellis. The wider project is joint work with Grant Passmore.

For further details, see a recent paper presented at the 2007 Workshop on Automated Formal Methods: http://homepages.inf.ed.ac.uk/pbj/papers/afm07.pdf