TRACER: A Symbolic Execution Tool for Verification

Joxan Jaffar, Vijayaraghavan Murali, Jorge Navas and Andrew Santosa


We present TRACER, a verifier for finite-state safety properties of se- quential C programs. It is based on symbolic execution (SE) and its unique fea- tures are in how it makes SE finite in presence of unbounded loops and its uses of interpolants to tackle the path-explosion problem.