Shape analysis for unstructured sharing (joint work with Huisong Li and Bor-yuh Evan Chang)

Abstract

Shape analysis aims to infer precise structural properties of imperative memory states and has been applied heavily to verify safety properties on imperative code over pointer-based data structures. It is often applied to dynamic structures such as lists and trees, that can be summarised using inductive predicates. Unfortunately, data structures with unstructured sharing, such as graphs, are challenging to describe and reason about in such frameworks. In particular, when the sharing is unstructured, it cannot be described inductively and in a purely local manner. In this talk, we will describe a global abstraction of sharing based on set-valued variables that when integrated with inductive definitions enables the specification and shape analysis of structures with unstructured sharing.

Short bio

Xavier Rival is a Senior Research Scientist (Directeur de Recherche) at INRIA Paris-Rocquencourt. His research interest focus on abstract interpretation and software verification by static analysis. He is mainly working on symbolic abstractions (trace partitionning abstraction, shape analysis, separation logic and memory abstract domains). He has been involved in the design, implementation and transfer of the Astrée analyser, a static analyser able to verify safety properties on industrial size safety critical softwares. He is currently the PI of the MemCAD ERC Starting Grant, aiming at the design of a library of abstract domains to describe memory states containing a wide range of complex data structures. He is also the Head of the ANTIQUE INRIA group, located at ENS Paris.