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 - Paris
                 2 rue Simone Iff (ou: 41 rue du Charolais)
                          Salle Lions 1, bâtiment C

                             Lundi 5 mars, 10h30

                                 -----------
                                 Hugo Illous
                                 -----------

                                     ENS

                      ==================================
                      A Relational Shape Abstract Domain
                      ==================================

Static analyses aim at inferring semantic properties of programs. While
many analyses compute an over-approximation of reachable states, some
analyses compute a description of the input-output relations of programs.
In the case of numeric programs, several analyses have been proposed that
utilize relational numerical abstract domains to describe relations. On
the other hand, designing abstractions for relations over memory states
and taking shapes into account is challenging. In this paper, we propose a
set of novel logical connectives to describe such relations, which are
inspired by separation logic. This logic can express that certain memory
areas are unchanged, freshly allocated, or freed, or that only part of the
memory was modified. Using these connectives, we build an abstract domain
and design a static analysis that over-approximates relations over memory
states containing inductive structures. We implement this analysis and
report on the analysis of a basic library of list manipulating functions.