Email Gateway (Aug 22 2022 at 14:00): Email Gateway (Aug 22 2022 at 14:00):From: Tobias Nipkow <nipkow@in.tum.de>
Infeasible Paths Elimination by Symbolic Execution Techniques: Proof of
Correctness and Preservation of Paths
Romain Aissat, Frederic Voisin and Burkhart Wolff
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.
Enjoy!
smime.p7s
Last updated: Apr 20 2024 at 12:26 UTC