Informatik, TU Wien

MemCAD: A Modular Abstract Domain for Reasoning on Memory States

In this talk, Xavier Rival presents the MemCAD analyzer, which relies on a parametric abstract domain for the static analysis by abstract interpretation of programs which manipulate complex and dynamically allocated data-structures.

Abstract

In this talk, Xavier Rival presents the MemCAD analyzer, which relies on a parametric abstract domain for the static analysis by abstract interpretation of programs which manipulate complex and dynamically allocated data-structures. He sets up the foundations for a family of static analyses to compute an over-approximation of the reachable states of programs using such structures, using modular abstractions, which can be adapted to wide families of programs.

A domain can be parameterized with a set of inductive definitions capturing a set of relevant datastructures 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. In the first part of his talk, Xavier Rival describes the abstraction induced by this domain, and the main static analysis operators. In particular, he considers 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.

In the second part, Xavier Rival considers several applications of his static analysis and shows how it can be adapted in order to treat specific features of programs written in languages which allow low level memory operations, such as the C language in a precise way. Finally, Rival focuses on recent work to extend the analysis to embedded softwares, which use a custom allocation inside static blocks, and manages its own dynamic structures inside this scope.

Biography

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 has been a member of the Abstraction group joint with Ecole Normale Supérieure (Paris) and CNRS.

Rival 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. Rival 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.

Note

This talk is organized by the Compilers and Languages Group at the Institute of Computer Languages.
Tea at the library of E185/1, Argentinierstr. 8, 4th floor (central) at 14:30.