Mickaël Delahaye

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:

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:

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