Accurate Theorem Proving for Program Verification

Symbolic software verification engines such as

Slam

and

ESC/Java

often use automatic theorem provers to implement forms of symbolic simulation. The theorem provers that are used, such as

Simplify

, usually combine decision procedures for the theories of uninterpreted functions, linear arithmetic, and sometimes bit vectors using techniques proposed by Nelson-Oppen or Shostak. Programming language constructs such as pointers, structures and unions are not directly supported by the provers, and are often encoded imprecisely using axioms and uninterpreted functions.

In this paper we describe a more direct and accurate approach towards providing symbolic infrastructure for program verification engines. We propose the use of a theorem prover called

Cogent

, which provides better accuracy for ANSI-C expressions with the possibility of nested logic quantifiers. The prover’s implementation is based on a machine-level interpretation of expressions into propositional logic.

Cogent

’s translation allows the program verification tools to better reason about finite machine-level variables, bit operations, structures, unions, references, pointers and pointer arithmetic.

This paper also provides experimental evidence that the proposed approach is practical when applied to industrial program verification.