@article{BM9,
title = { Refinement to Certify Abstract Interpretations: Illustrated on Linearization for Polyhedra },
author = {Boulm\'e, Sylvain and Mar\'echal, Alexandre},
year = {2019},
journal = {Journal of Automated Reasoning},
number = {4},
pages = {505--530},
volume = {62},
team = {PACSS, axe_FormalProofs},
abstract = {Our concern is the modular development of a certified static analyzer in the Coq proof assistant. We focus on the extension of the Verified Polyhedra Library---a certified abstract domain of convex polyhedra---with a linearization procedure to handle polynomial guards. Based on ring rewriting strategies and interval arithmetic, this procedure partitions the variable space to infer precise affine terms which over-approximate polynomials. In order to help formal development, we propose a proof framework, embedded in Coq, that implements a refinement calculus. It is dedicated to the certification of parts of the analyzer---like our linearization procedure---whose correctness does not depend on the implementation of the underlying certified abstract domain. Like standard refinement calculi, it introduces data-refinement diagrams. These diagrams relate ``abstract states'' computed by the analyzer to ``concrete states'' of the input program. However, our notions of ``specification'' and ``implementation'' are exchanged w.r.t. standard uses: the ``specification'' (computing on ``concrete states'') refines the ``implementation'' (computing on ``abstract states''). Our stepwise refinements of specifications hide several low-level aspects of the computations on abstract domains. In particular, they ignore that the latter may use hints from external untrusted imperative oracles (e.g. a linear programming solver). Moreover, refinement proofs are naturally simplified thanks to computations of weakest preconditions. Using our refinement calculus, we elegantly define our partitioning procedure with a continuation-passing style, thus avoiding an explicit datatype of partitions. This illustrates that our framework is convenient to prove the correctness of such higher-order imperative computations on abstract domains.},
}
