IMDEA Software

Iniciativa IMDEA

Inicio > Eventos > Charlas Invitadas > 2010 > Shape analysis using separating shape graphs
Esta página aún no ha sido traducida. A continuación se muestra la página en inglés.

Xavier Rival

martes 13 de abril de 2010

11:00am IMDEA conference room

Xavier Rival, Researcher, École Normale Supérieure, Paris, France

Shape analysis using separating shape graphs


The purpose of shape analysis is to infer properties about unbounded data structures, such as trees or lists. We will present a shape analysis based on abstract inerpretation, which uses separation logic and inductive definitions. Our analysis targets C programs. The elements of our abstract domain can be seen as separation logic formulae or equivalently as separating shape graphs. It is parametric in the inductive definitions of the structures ti be used for a given analysis.

We will present the definition of this abstract domain together with the main analysis algorithms such as materialization (local concretization) and widening (global abstraction) and our recent progress for accomodating low level aspects of the C language.