Verimag polyhedra library

A verified abstract domain of polyhedra

I built the Verimag polyhedra library, shortened VPL, while investigating building an abstract domain of polyhedra for the Verasco static analyzer. This research work spans a few different fields.

VPL is implemented in Coq and Ocaml and is competitive in performance with existing polyhedra libraries, when used for analyzing C programs. The Ocaml code is itself a complete abstract domain which results are simply checked in Coq. Snapshots of the code are currently available for download.

Academic publications

The theoretical and design parts of my work on VPL are described in the following publications.