A Refinement Calculus to certify
impure abstract computations
of the Verimag Polyhedra Library


This page presents the work of Sylvain Boulmé and Alexandre Maréchal about:

Our approach is described in this paper, also available on HAL. In 2018, this has been published in JAR (Journal of Automated Reasoning) (see also the corresponding doi) and extends a previous version of ITP 2015.

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.

Source code

The last version of the code is now on our github repository. The original version is still available here.