Edinburgh Research Explorer

Using SMT solvers to verify high-integrity programs

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Original languageEnglish
Title of host publicationProceedings of the second workshop on Automated formal methods
Place of PublicationNew York, NY, USA
PublisherACM
Pages60-68
Number of pages9
ISBN (Print)978-1-59593-879-4
DOIs
Publication statusPublished - 2007

Publication series

NameAFM '07
PublisherACM

Abstract

In this paper we report on our experiments in using the currently popular Smt (Sat Modulo Theories) solvers Yices [10] and Cvc3 [1] and the Simplify theorem prover [9] to discharge verification conditions (VCs) from programs written in the Spark language [5]. 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 generator and an automatic prover for VCs.

We find that Praxis's prover can prove more VCs than Yices, Cvc3 or Simplify because it can handle some relatively simple non-linear problems, though, by adding some axioms about division and modulo operators to Yices, Cvc3 and Simplify, we can narrow the gap. One advantage of Yices, Cvc3 and Simplify is their ability to produce counterexample witnesses to VCs that are not valid.

This work is the first step in a 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. For example, we are interested in improving support for non-linear arithmetic and automatic loop invariant generation.

ID: 6336974