Infeasible Paths Elimination by Symbolic Execution Techniques: Proof of Correctness and Preservation of Paths

Romain Aissat, Frederic Voisin and Burkhart Wolff 📧

August 18, 2016

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Abstract

TRACER 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.

License

BSD License

Topics

Session InfPathElimination