Scottish Theorem Proving Meeting
@ Heriot-Watt University

30 November 2007

Organisers: Andrew Ireland, Lilia Georgieva

Location

Earl Mountbatten Building
Heriot-Watt University, Room 2.33
Riccarton
Edinburgh, EH14 4AS
How to get here

Programme

13.00 Lunch in Scholars
Please contact
Lilia Georgieva if you intend to come to lunch.
14.00 Ianthe Hind Making Smallfoot Extensible


The Smallfoot family of tools support the automatic verification of shape properties specified in separation logic. Our aim is to make these tools extensible by adding the ability to add new user-defined inductive predicates on the fly. We believe this will require co-operation with proof planning via middle-out reasoning and proof patching.
14.45 Alice Miller Advanced Symmetry Reduction Tools for Model Checking


We have recently been awarded an EPSRC grant (ARTE) to extend our work on symmetry reduction tools for model checking. In this talk I will summarise our previous work and describe what we intend to do in ARTE. This includes developing a symmetry reduction tool for the probabilistic modelf checker LiQuor (or for our own purpose-built explicit state probabilistic model checker) and extending our symmetry reduction tool for Spin, TopSpin.
15.30 Coffee in Room 2.33
16.15 Paul Jackson A comparison of automatic theorem provers for proving verification conditions derived from SPARK-Ada programs

SPARK is a subset of Ada used primarily in high-integrity systems in the aerospace, defence, rail and security industries. Formal verification of SPARK programs is supported by tools produced by the UK company Praxis High Integrity Systems. These tools include a VC (verification condition) generator and an automatic prover for VCs. The provers compared include Praxis's prover, the Simplify prover used in the ESC/Java Java static program verifier, and the SMT (SAT Modulo Theories) solvers Yices and CVC3. SMT solvers have been improving rapidly in the last few years and are invigorating a variety of lines of research into formal verification tools. One main observation is that Praxis's prover can prove more VCs than the other provers considered 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. This work builds on immediate previous work by Kathleen Sharp and Bill Ellis. 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 wider project is joint work with Grant Passmore. Where possible it will draw on the previous experiences of Bill Ellis and Andrew Ireland in using proof planning and recursion analysis to derive and prove loop invariants for SPARK programs. For further details, see a recent paper presented at the 2007 Workshop on Automated Formal Methods:

Using SMT Solvers to Verify High Integrity Programs


17.00 Meeting ends

Previous STP seminars
For further information please contact: Lilia Georgieva