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.
- 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.
Academic publications
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