TRACER: A Symbolic Execution Tool for Verification

NUS logo

Description

TRACER is a verification tool based on symbolic execution for finite-state C sequential programs developed at National University of Singapore .
TRACER attempts at building a finite symbolic execution tree which overapproximates the set of all concrete reachable states. 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.
TRACER computes interpolants (using weakest preconditions among other methods) from infeasible paths and 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 under active development.
Any feedback is welcome and feel free to email Vijayaraghavan Murali for any question/enquiry.