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

Description

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

• a refinement calculus (i.e. a proof framework based on the lattice algebra of predicate transformers) dedicated to the certification of computations on a polyhedra abstract domain;
• and its application to the certification in Coq of an interval-based linearization procedure.

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.