Automatic proof of SPARK verification conditions

Add to your list(s) Download to your calendar using vCal

• Paul Jackson (School of Informatics, University of Edinburgh)
• Tuesday 11 December 2007, 13:00-14:00
• Computer Laboratory, William Gates Building, Room SS03.

If you have a question about this talk, please contact Thomas Tuerk.

This talk has been canceled/deleted

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

This talk is part of the Computer Laboratory Automated Reasoning Group Lunches series.

This talk is included in these lists:

This talk is not included in any other list

Note that ex-directory lists are not shown.