|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
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:
For further information please contact: Lilia Georgieva