IPEG (Infeasible Path Explanation and Generalization) is a proprietary dynamic symbolic execution tool to experiment infeasible path generalization. From a program written in a significant subset of the C language, IPEG is able:
- to find the program infeasible paths via symbolic execution;
- to analyze path condition to explain path infeasibility;
- to generalize a (potentially infinite) family of infeasible paths as an automaton based on the explanation of a single infeasible path;
- to combine infeasible path automaton.
And, with its more than 10KLOC of OCaml and Prolog, IPEG can actually generate test inputs efficiently by skipping a lot of infeasible paths.
IPEG connects to any constraint solver, to date:
- CEA Colibri, CLP solver
- ECLiPSe IC, CLP solver
- Yices, SMT solver (via my own Ocaml binding)
- Microsoft Z3, SMT Solver
IPEG also uses static information issued by Frama-C, an open source static analysis framework.