Romain Aissat, Frederic Voisin and Burkhart WolffTRACER is a tool for verifying safety properties of sequential C programs. TRACER attempts at building a finite symbolic execution graph which over-approximates the set of all concrete reachable states and the set of feasible paths. We present an abstract framework for TRACER and similar CEGAR-like systems. The framework provides 1) a graph- transformation based method for reducing the feasible paths in control-flow graphs, 2) a model for symbolic execution, subsumption, predicate abstraction and invariant generation. In this framework we formally prove two key properties: correct construction of the symbolic states and preservation of feasible paths. The framework focuses on core operations, leaving to concrete prototypes to âfit inâ heuristics for combining them. The accompanying paper (published in ITP 2016) can be found at https://www.lri.fr/âwolff/papers/conf/2016-itp-InfPathsNSE.pdf.
Description: S/MIME Cryptographic Signature