IPEG

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 screen shot showing an infeasible path automaton

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.

Experimental data

Benchmark programs: git_config, tcas (SIR), gcd, tritype, erfill, bsearch, merge, selection_sort, checkutf8