Testing, Abstraction, Theorem Proving: Better Together!

Greta Yorsh, Thomas Ball, and Mooly Sagiv

In Proc. International Symposium on Software Testing and Analysis, 2006 (ISSTA 2006)

We present a method for static program analysis that leverages tests and concrete program executions. State abstractions generalize the set of program states obtained from concrete executions. A theorem prover then checks that the generalized set of concrete states covers all potential executions and satisfies additional safety properties. Our method finds the same potential errors as the most-precise abstract interpreter for a given abstraction and is potentially more efficient. Additionally, it provides a new way to tune the performance of the analysis by alternating between concrete execution and theorem proving. We have implemented our technique in a prototype for checking properties of C# programs.

Click here to access the full version of the paper (including proofs): PostScript; PDF