To: seminaire-gallium-moscova@inria.fr From: Francois.Pottier@inria.fr Subject: SEM - INRIA : Gallium - 05/05/08 - Paris - FR Vous pouvez vous abonner à nos annonces de séminaires http://pauillac.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 5 mai, 10h30 ------------ Xavier Rival ------------ INRIA ==================================================== Shape analysis based on inductive invariant checkers ==================================================== Shape analyses allow to infer precise information about the runtime memory layout of programs. This allows to early discover various kinds of bugs in programs or to prove formally their memory safety. We will present a shape analysis based on abstract interpretation, which uses a parametric abstract domain, where the structures that should be tracked are supplied by the user. We will describe our abstract domain and the elementary operations for our analysis. In particular, an unfolding operation locally refines the abstraction, in order to make it possible to analyze elementary program features, whereas a folding operation performs a global abstraction, which is essential to ensure termination. Last, the domain abstracting shapes will be extended, so as to deal with values in the environment and to further extend the expressivity of the abstraction.