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.

My work served as the basis for other projects. The current state of things and associated code can be found here and here.

Academic publications

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