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.

- Static analysis of computer programs. Polyhedra are used to handle linear relations between the value of variables, such as x <= y + 2. For example, such relations hold in the body of tests: if(x < = y + 2) { … /* holds here */ }.
- Computational geometry. Polyhedra are geometrical objects: a cube is a kind of polyhedron. Using them for static analysis requires performs various transformations on them, like projection, intersection, convex hull.
- Linear optimisation. This is the field of computer-assisted decision making. It originated from production planning in the 1950s with the simplex algorithm. “Linear” means that these algorithms are looking for a point of a polyhedron which maximises a user-defined quantity. It is used in VPL for deciding inclusions.
- Formal proof. The Verasco static analyzer comes with the proof that all that it says about a program is true. This proof is written using the Coq proof assistant. Although this is more work than making proofs on paper, the resulting guarantees are much stronger. Sylvain Boulmé and I proved correct the operators of the VPL.

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.

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

- Polyhedral approximation of multivariate polynomial using Handelman's theorem with Alexandre Maréchal, Tim King, David Monniaux and Michaël Périn at the International Conference on Verification, Model Checking and Abstract Interpretation 2016
- Revisiting the abstract domain of polyhedra: constraint-only representation and formal proof, Ph.D. thesis, 2015
- A certifying frontend for (sub)polyhedral abstract domains, with Sylvain Boulmé at the Working Conference on Verified Software: Theories, Tools and Experiments 2014
- Modular and lightweight certification of polyhedral abstract domains, with Michaël Périn and Sylvain Boulmé, as an extended abstract for the Types Meeting 2014
- Efficient generation of correctness certificates for the abstract domain of polyhedra, with David Monniaux and Michaël Périn at the Static Analysis Symposium 2013