TRACER: A Symbolic Execution Tool for Verification |
TRACER attempts at building a symbolic execution tree. If the error location cannot be reached from any symbolic path then the program is reported as safe. Otherwise, either the program may contain a bug or it may not terminate. TRACER reports a false alarm only if the theorem prover fails to prove a valid claim.
The most innovative features of TRACER stem from how it tackles
the two fundamental limitations of symbolic execution: exponential
number of paths on the number of program branches, and
infinite-length symbolic paths due to unbounded loops.
To tackle the first problem, TRACER computes Craig interpolants
from infeasible paths to be used in generalizing visited state,
that can then be further used to subsume other paths.
To tackle the second problem, it integrates a novel
counterexample-guided refinement phase within the symbolic execution
process.