TRACER: A Symbolic Execution Tool for Verification

NUS logo

Description

TRACER is a verification tool based on symbolic execution for sequential C programs developed at National University of Singapore .

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.

Implementation of TRACER
TRACER Pipeline

Papers based on TRACER


Download/Installation


People


Contact

TRACER is currently under sporadic development. Its source code is now available here
Any feedback is welcomed and please email Joxan Jaffar (joxan AT comp DOT nus DOT edu DOT sg) for any question/enquiry.