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.