TRACER: A symbolic execution tool for verification
Joxan Jaffar, Vijayaraghavan Murali, JA Navas, AE Santosa · 2012
Abstract. We present TRACER, a verifier for finite-state safety properties of sequential C programs. It is based on symbolic execution (SE) and its unique features are in how it makes SE finite in presence of unbounded loops and its uses of interpolants to tackle the path-explosion problem. 1