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 MARDI 14 octobre, 10h30 ---------------- Antoine Toubhans ---------------- ENS ============================================= Composite Abstract Domains for Shape Analysis ============================================= In this talk, I will present the research work I have been carrying out over the last 3 years as part of the MemCAD project during my PhD. The MemCAD project aims at designing a static analysis of programs manipulating complex realistic memories that include a wide range of data structures such as arrays, strings, dynamically-allocated linked data structures (linked lists, trees, ...). We are interested in proving memory safety properties (e.g. the absence of null pointer dereferences, memory leaks, incorrect memory freeing) and verifying data structure invariants. Our analysis is based on the abstract interpretation framework, that allows to compute an over-approximation (superset) of the concrete semantics of programs. Specifically, the analysis computes a finite representation of a superset of the set of reachable memory states for each program point. It relies on an abstract domain that is a predicate algebra providing finite representations of (infinite) set of memory states along with abstract transfer functions. Many efforts have been made to design new abstract domains over the last decades. Therefore, the breadth and depth of data structures that can be handled by the union of today's shape analyses is quite astounding. However, no framework allows to deal with all of them in a single analysis. To cope with that issue, we developed techniques to combine several existing abstract domains into more complex ones and implemented these combinators into the MemCAD analyzer. In this talk, I will present two combinators: 1) the separating product of memory abstract domains, that applies different abstractions on disjoint memory chunks 2) the reduced product of memory abstract domains, that represents concrete memories by (classical) conjunctions of abstract elements and that enables communication between the components of the product.