BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Automatic proof of SPARK verification conditions - Paul Jackson (S
 chool of Informatics\, University of Edinburgh)
DTSTART:20071211T130000Z
DTEND:20071211T140000Z
UID:TALK9410@talks.cam.ac.uk
CONTACT:Thomas Tuerk
DESCRIPTION:SPARK is a subset of Ada used primarily in high-integrity syst
 ems in the aerospace\, defence\, rail and security industries. In this tal
 k 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.\n\nWe 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 opera
 tors 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.\n\nThe work is the first step in a wider project to i
 ncrease the fraction of VCs from current SPARK programs that can be proved
  automatically and to broaden the range of properties that can be automati
 cally checked. Project interests include improving support for non-linear 
 arithmetic and for automatic loop invariant generation.\n\nThis work build
 s on previous work by Kathleen Sharp and Bill Ellis. The wider project is 
 joint work with Grant Passmore.\n  \nFor further details\, see a recent pa
 per presented at the 2007 Workshop on Automated Formal Methods:\nhttp://ho
 mepages.inf.ed.ac.uk/pbj/papers/afm07.pdf\n
LOCATION:Computer Laboratory\, William Gates Building\, Room SS03
END:VEVENT
END:VCALENDAR