Infeasible paths elimination by symbolic execution techniques: Proof of correctness and preservation of paths

Abstract

TRACER [8] 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 [2,3,5,6,9]. The framework provides (1) a graphtransformation 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.