### 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

- Computer science/Programming languages/Static analysis

### Session InfPathElimination

- Graph
- Aexp
- Bexp
- Labels
- Store
- Conf
- SymExec
- LTS
- SubRel
- ArcExt
- SubExt
- RB

## Cite

×

InfPathElimination-AFP

    @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   = {August},
      year    = {2016},
      note    = {\url{https://isa-afp.org/entries/InfPathElimination.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Aug 18, 2016 : Isabelle2016