This page presents the work of Sylvain Boulmé and Alexandre Maréchal about:
This work on a certified abstract domain of polyhedra extends previous works with Alexis Fouilhé, still available here.
With Michaël Périn, we had previously proposed to apply refinement for certifying abstract interpreters (see Simple Certificates for static Analysis with code Transformations). While based on similar ideas, the present proposition is much more flexible: the framework does not require a global certificate from the analyzer. Of course, it still allows "local" certificates, i.e. a-posteriori certification of results from oracles.
The last version of the code is now on our github repository. The original version is still available here.