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

 

Title: Infeasible Paths Elimination by Symbolic Execution Techniques: Proof of Correctness and Preservation of Paths
Authors: Romain Aissat, Frederic Voisin and Burkhart Wolff ( wolff /at/ lri /dot/ fr)
Submission date: 2016-08-18
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.
BibTeX:
@article{InfPathElimination-AFP,
  author  = {Romain Aissat and Frederic Voisin and Burkhart Wolff},
  title   = {Infeasible Paths Elimination by Symbolic Execution Techniques: Proof of Correctness and Preservation of Paths},
  journal = {Archive of Formal Proofs},
  month   = aug,
  year    = 2016,
  note    = {\url{http://isa-afp.org/entries/InfPathElimination.shtml},
            Formal proof development},
  ISSN    = {2150-914x},
}
License: BSD License