Vous pouvez vous abonner à nos annonces de séminaires http://gallium.inria.fr/seminaires/ S E M I N A I R E __ / _` _ / / o /| /| __ __ __ __ _ _ / ) __) / / / / / /\/| ----- / |/ | / )(_ / / ) ) ) __) (___/ (_/ (_ (_ / (__/ / | / | (__/ __)(_ (__/ (_/ (_/ I N R I A - Rocquencourt Amphi Turing du bâtiment 1 Lundi 10 janvier, 10h30 --------------- David Pichardie --------------- INRIA ================================= Certified Abstract Interpretation ================================= Nowadays safety critical systems are validated through long and costly test campaigns. Static analysis is a promising complementary technique that allows to automatically prove the absence of restricted classes of bugs. A significant example is the state-of-the-art ASTRÉE static analyzer for C which has proven some critical safety properties for the primary flight control software of the Airbus A340 fly-by-wire system. Taking note of such a success, the next question is: should we completely remove the test campaign dedicated to the same class of bugs? If we trust the result of the analyzer, of course the answer is yes, but should we trust it? The analyzer itself can be certified by testing, but exhaustivity cannot be achieved. In this work, we show how mechanized proofs can be used to certify static analyzers or their results. Proof assistants allow to mechanically specify, program and prove correct static analyzers with respect to a formal model of the programming language semantics. If the feasibility of such a technique has been demonstrated for various kinds of analyses and programming languages, none of them has handled relational abstract domain with convergence acceleration by widening. A complex static analyzer like ASTRÉE is an assembly of several such abstract domains. Each domain has a specific task, i.e. the discovery of program properties in a specific range and communicate with the other domains in order to obtain a more precise global diagnostic. As a consequence, extending such a tool with a new abstract domain is a risky adventure: a buggy abstract domain may propagate unsound information that invalidates the whole result of the analyser. In this work, we propose a formal framework for the formal development of certified abstract interpreters in Coq. We provide an abstract interpreter for a simple imperative language and a lattice library for modular construction of abstract domains. We conclude with our ongoing work about the formalization of relational abstract domains.