ROSAEC center Seoul National University

Seminars & Workshops

Speaker:Xavier Rival , École Normale Supérieure
When:2011-08-26 13:00
Place:Room 309, Bldg 302, SNU


In this talk, we will present a parametric abstract domain for the static analysis by abstract interpretation of programs which manipulate complex and dynamically allocated data-structures. We will set up the foundations for a family of static analyses to compute an over-approximation of the reachable states of programs using such structures. Our domain can be parameterized with a set of inductive definitions capturing a set of relevant data-structures and by the choice of an underlying numerical domain. Abstract values can be viewed either as graphs, or as formulas in a subset of separation logic extended with inductive definitions. We will describe the abstraction induced by this domain, and the main static analysis operators. In particular, we will consider the unfolding operator, which allows to refine in a local manner an abstract value, so as to allow precise algorithms for the computation of post-conditions. Then, we will discuss a set of join and widening operators, so as to guarantee the termination of our static analyses. In the second part of the talk, we will consider several applications of our static analysis. We will show how it can be adapted in order to treat in a precise way specific features of programs written in languages which allow low level memory operations, such as the C language. Then, we will focus on the analysis of programs with recursive procedures and we will introduce a powerful widening operator, which is able to infer accurate inductive definitions to be used to summarize the call-stack of a specific program together with the memory. Finally, the last part of this talk will be devoted to perspectives for extensions of our analysis.

Short bio

Xavier Rival studied at Ecole Normale Superieure (Paris, France) and prepared his PhD Thesis under the supervision of Patrick Cousot. After defending his PhD in 2005, he worked as a Post Doctorate researcher at University of California at Berkeley from 2006 to 2007. Then, he joined Inria as a Junior Researcher in 2007, as part of the "Abstraction" project team. He also holds a part time Lecturer position at Ecole Polytechnique (Paris, France). He has also been a member of the Astree project since its beginning in 2001. Xavier Rival also defended his Habilitation Thesis in 2011. He is interested in static analysis using abstract interpretation technique. Over the last few years, he has mainly been studying the static analysis of programs manipulating complex data-structures. including the best paper award at the USENIX Security Symposium and the highest ranked paper at the IEEE Symposium on Security and Privacy.


© Copyright 2008-2010 ROSAEC Center, Seoul National University