Symbolic software analysis engines such as SLAM and ESCJava 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 therefore they 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 analysis 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 analysis 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 analysis
Submitted for publication, a copy is available upon request, 2004, 15 pages.
© 2004 Natasha Sharygina.