Veranstaltungen

04. September 2012, 15:15 bis 00:00

Dr. Xavier Rival: MemCAD, a Modular Abstract Domain for Reasoning on Memory States

Vortrag

In this talk, we will present the MemCAD analyzer, which relies on aparametric abstract domain for the static analysis by abstractinterpretation of programs which manipulate complex and dynamicallyallocated data-structures. We will set up the foundations for a familyof static analyses to compute an over-approximation of the reachablestates of programs using such structures, using modular abstractions,which can be adapted to wide families of programs.

Our domain can be parameterized with a set of inductive definitionscapturing a set of relevant data-structures and by the choice of anunderlying numerical domain. Abstract values can be viewed either asgraphs, or as formulas in a subset of separation logic extended withinductive definitions. We will describe the abstraction induced bythis domain, and the main static analysis operators. In particular, wewill consider the unfolding operator, which allows to refine in alocal manner an abstract value, so as to allow precise algorithms forthe computation of post-conditions. Then, we will discuss a set ofjoin and widening operators, so as to guarantee the termination of ourstatic analyses.

In the second part of the talk, we will consider several applicationsof our static analysis. We will show how it can be adapted in order totreat in a precise way specific features of programs written inlanguages which allow low level memory operations, such as the Clanguage. Then, we will focus on the analysis of programs withrecursive procedures and we will introduce a powerful wideningoperator, which is able to infer accurate inductive definitions to beused to summarize the call-stack of a specific program together withthe memory.

Finally, the last part of this talk will focus on recent work toextend the analysis to embedded softwares, which use a customallocation inside static blocks, and manages their own dynamicstructures inside this scope. The reason for this programming patternis that dynamic memory allocation should not be used in highlycritical avionic softwares. It brings new issues for the verificationof software by static analysis, which can be addressed using ourmodular abstraction.

Kurzbiographie von Xavier Rival

Xavier Rival studied at Ecole Normale Supérieure (Paris) and obtainedhis PhD in 2005 from Ecole Polytechnique. He worked as aPost-doctorate researcher at the University of California atBerkeley. He joined INRIA as a Junior Research Scientist in 2007 andhe has been a member of the Abstraction group joint with Ecole NormaleSupérieure (Paris) and CNRS.  He holds a Lecturer position at EcolePolytechnique since 2009. His main research topic is static analysisof safety critical programs using abstract interpretation techniques,and he took part to the design and implementation of the Astree staticanalyzer. He also worked on certified compilation. More recently, hestarted working on static analyses for the verification of memoryproperties of programs that manipulate complex data-structures. ( <link www.di.ens.fr/~rival/ _blank>http://www.di.ens.fr/~rival/</link> )

Kalendereintrag

Veranstaltung Details

Öffentlich
Ja
Kostenpflichtig
Nein
Anmeldung erforderlich
Nein