Using SMT solvers to verify high-integrity programs

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.