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

  Browse A-Z

Log in

Cambridge users (raven)details Other usersdetails No account?details

Information on

Subscribing to talksdetails Finding a talkdetails Adding a talkdetails Disseminating talksdetails Help and Documentationdetails

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.

Other lists

First Intestinal Epithelial Research Symposium Travel and Expeditions Thinking Society: Is our university a place of free thinking?

Other talks

Stereodivergent Catalysis, Strategies and Tactics Towards Secondary Metabolites as enabling tools for the Study of Natural Products Biology Childhood adversity and chronic disease: risks, mechanisms and resilience. Numerical solution of the radiative transfer equation with a posteriori error bounds Babraham Lecture - Deciphering the gene regulation network in human germline cells at single-cell & single base resolution Gaze and Locomotion in Natural Terrains Kolmogorov Complexity and Gödel’s Incompleteness Theorems Networks, resilience and complexity Protein Folding, Evolution and Interactions Symposium Direct measurements of dynamic granular compaction at the mesoscale using synchrotron X-ray radiography Investigating the Functional Anatomy of Motion Processing Pathways in the Human Brain PTPmesh: Data Center Network Latency Measurements Using PTP Perylene-Based Poly(N-Heterocycles): Organic Semiconductors, Biological Fluorescence Probes and Building Blocks for Molecular Surface Networks
 

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