Small Witnesses for Abstract Interpretation-Based Proofs

11 years 6 months ago
Small Witnesses for Abstract Interpretation-Based Proofs
tnesses for Abstract Interpretation-based Proofs Fr´ed´eric Besson, Thomas Jensen, and Tiphaine Turpin IRISA/{Inria, CNRS, Universit´e de Rennes 1} Campus de Beaulieu, F-35042 Rennes, France Abstract. Abstract interpretation-based proof carrying code uses postts of abstract interpretations to witness that a program respects a safety policy. Some witnesses carry more information than needed and are therefore unnecessarily large. We introduce a notion of size of a witness and propose techniques for reducing the size of such certificates. For distributive analyses, we show that a smallest witness exist and we give an iterative algorithm for computing it. For non-distributive analyes we propose a technique for pruning a witness and illustrate this pruning on a relational, polyhedra-based analysis. Finally, only the existence of a witness is needed to assure the code consumer of the safety of a given program. This makes possible a compression technique of witnesses where only part of a ...
Frédéric Besson, Thomas P. Jensen, T
Added 07 Jun 2010
Updated 07 Jun 2010
Type Conference
Year 2007
Where ESOP
Authors Frédéric Besson, Thomas P. Jensen, Tiphaine Turpin
Comments (0)