University of Cambridge > Talks.cam > Computer Laboratory Automated Reasoning Group Lunches > Automatic proof of SPARK verification conditions

Automatic proof of SPARK verification conditions

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

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

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2017 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity