Title: Modular Construction of Shape-Numeric Analyzers

Speaker: Xavier Rival (INRIA Paris-Rocquencourt, France)

　　    www.di.ens.fr/~rival/

Time: 10:00, 18th November 2013

Venue: Lecture Room, 3rd Floor, Building #5, State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences

Abstract:

The aim of static analysis is to infer invariants about programs that are precise enough to establish semantic properties, such as the absence of run-time errors. Broadly speaking, there are two major branches of static analysis for imperative programs. Pointer and shape analyses focus on inferring properties of pointers, dynamically allocated memory, and recursive data structures, while numeric analyses seek to derive invariants on numeric values. Although simultaneous inference of shape-numeric invariants is often needed, this case is especially challenging and is not particularly well explored. Notably, simultaneous shape-numeric inference raises complex issues in the design of the static analyzer itself.

In this talk, we will study the construction of such shape-numeric, static analyzers. We set up an abstract interpretation framework that allows us to reason about simultaneous shape-numeric properties by combining shape and numeric abstractions into a modular, expressive abstract domain. Such a modular structure is highly desirable to make its formalization and implementation easier to do and get correct. To achieve this, we choose a concrete semantics that can be abstracted step-by-step, while preserving a high level of expressiveness. The structure of abstract operations (i.e., transfer, join, and comparison) follows the structure of this semantics. The advantage of this construction is to divide the analyzer in modules and functors that implement abstractions of distinct features.

Biography:

Xavier Rival is Research Scientist at INRIA Paris-Rocquencourt. He is a member of the Abstraction Project team, a joint group with CNRS and Ecole Normale Supérieure. He obtained a PhD in Computer Science at Ecole Polytechnique in 2005 and an Habilitation Thesis in Computer Science at Ecole Normale Superieure in 2011. He is working on abstract interpretation based static analysis techniques, and in particular on symbolic abstract domains. He has been involved in the Astree project since its beginning in 2001. Since 2011, he is the PI of the MemCAD ERC project, for the design of memory abstract domains.