Modular Proof Principles for Parameterised Concretizations

Abstract. Abstract interpretation is a particularly well-suited methodology to build modular correctness proof of static analysers. Proof modularity becomes essential when correctness proof is machine checked for c languages To deal with complex concrete and abstract domains, the notion of parameterised concretization has been proposed to allow a al decomposition of the abstract domain and its concretization. In this paper we develop proof principles for such concretizations, based on the theoretical notion of concretization functor, with the aim of obtaining modular correctness proofs. Our technique has been tested on a machine-checked correctness proof of a static analysis for a Java-like bytecode language.

• Type: Conference
• Year: 2005
• Where: CASSIS
• Authors: David Pichardie
• Keywords: CASSIS 2005, Correctness Proof, Human Computer Interaction, Machine-checked Correctness Proof, Modular Correctness Proofs