Using SMT solvers to verify high-integrity programs

Paul B. Jackson, William James Ellis, Kathleen Sharp

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

8 Citations (Scopus)

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. Copyright 2007 ACM.

Original languageEnglish
Title of host publicationAFM'07: 2nd Workshop on Automated Formal Methods
Pages60-68
Number of pages9
DOIs
Publication statusPublished - 2007
Event2nd Workshop on Automated Formal Methods - Atlanta, GA, United States
Duration: 6 Nov 20076 Nov 2007

Conference

Conference2nd Workshop on Automated Formal Methods
Abbreviated titleAFM'07
CountryUnited States
CityAtlanta, GA
Period6/11/076/11/07

Keywords

  • Ada
  • SAT modulo theories solver
  • SMT solver
  • SPARK

Fingerprint Dive into the research topics of 'Using SMT solvers to verify high-integrity programs'. Together they form a unique fingerprint.

Cite this