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:

Our approach is described in this paper, also available on HAL (this is an extended version of an ITP 2015 paper, published in LNCS 9236).

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

You may download our source code in this archive. This archive contains a release of the VPL co-developed with Alexis Fouilhé. This release provides a toy but certified analyzer in order to run tests on the abstract domain (see file README in the archive). You may also run the VPL in releases of Verasco analyzer.

The build system requires GNU make. It also relies on the necessary tools being available in the PATH: ocamlc, ocamlopt, ocamldep, ocamldoc, ocamlfind, coqc, coqdep. The backend depends on the ZArith front-end to the GMP library and the Makefile relies on ocamlfind being configured so as to find it. It also depends on versions 8.4 of the Coq proof assistant. (see file README in the archive)

The contents of the source archive is licensed under the 2-clause BSD license (see file LICENSE in the archive).

This works is part of ANR Verasco.