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 ...

• Type: Conference
• Year: 2007
• Where: ESOP
• Authors: Frédéric Besson, Thomas P. Jensen, Tiphaine Turpin
• Keywords: Abstract Interpretation-based Proof, ESOP 2007, Programming Languages, Smallest Witness Exist, Witness