Institute of Computer Languages
Compilers and Languages Group

Talks 2011 - Xavier Rival

Der Arbeitsbereich für Programmiersprachen und Übersetzer am Institut für Computersprachen lädt zu folgendem Vortrag ein:

Dr. Xavier Rival

INRIA Roquencourt / Ecole Normale Supérieure (ENS Paris), Frankreich


A Parametric Shape Analysis based on User-supplied Inductive Definitions

Datum: September/Oktober 2011


We are going to present a parametric static analysis of programs that manipulate complex data-structures. This analysis aims at inferring complex invariants of programs using inductive and dynamically allocated data-structures, such as complex forms of lists or trees.

Our analysis utilizes user-supplied inductive definitions of the data-structures manipulated by the program, and infers complex invariants using those basic predicates. Our abstract domain relies on a fragment of separation logic with inductive definitions. It can also express low-level local properties, in C programs that perform complex operations at the byte level and capture high level invariants of recursive programs.

We will present our abstraction, and show the main analysis operations including the unfolding operation, which performs a local concretization of abstract predicates for the analysis of common statements and the widening operation, which performs a global abstraction and ensures the termination of the analysis.

(joint work with Bor-Yuh Evan Chang)

Kurzbiographie von Xavier Rival

Xavier Rival studied at Ecole Normale Supérieure (Paris) and obtained his PhD in 2005 from Ecole Polytechnique. He worked as a Post-doctorate researcher at the University of California at Berkeley. He joined INRIA as a Junior Research Scientist in 2007 and he has been a member of the Abstraction group joint with Ecole Normale Supérieure (Paris) and CNRS. He holds a Lecturer position at Ecole Polytechnique since 2009. His main research topic is static analysis of safety critical programs using abstract interpretation techniques, and he took part to the design and implementation of the Astree static analyzer. He also worked on certified compilation. More recently, he started working on static analyses for the verification of memory properties of programs that manipulate complex data-structures. (

Sie möchten auf diesen Vortrag durch Aushang hinweisen? Eine druckfertige Einladung im pdf-Format dafür finden Sie hier.

   About Us
      Talks 2017
      Talks 2016
      Talks 2015
      Talks 2014
      Talks 2013
      Talks 2012
      Talks 2011
      Talks 2010
      Talks 2009
      Talks 2008
      Talks 2007
      Talks 2006
      Talks 2005
      Talks 2004
Fast Access:
Previous Talk
Next Talk
Faculty of Informatics
Vienna University of Technology
top | HTML 4.01 | last update: 2017-02-13 (Webmaster)