Towards a modular memory abstraction

Abstract

Constructing an abstract domain able to express a complex set of properties is a hard task, as several difficulties have to be solved all together, including the choice of efficient data-structures, the design of efficient algorithms and the engineering of the whole construction. Experience with numerical abtract domains has shown that making abstract domains modular helps in addressing these problems. In this talk we are going to discuss how this principle can be implemented in memory abstractions. We will consider three ways of making memory abstractions modular. First, we will describe the splitting of the memory reasoning and of the value reasoning. Second, we will show a variant of a reduced product, which allows to express conjunctions of memory properties. Third, we will consider hierarchical abstraction of memory states, which allows to reason about certain nested data-structures patterns.

Short bio

Dr. Xavier Rival is a research scientist at INRIA Paris-Rocquencourt, and a member of Abstraction Project/Team joint with École Normale Supérieure (Paris) and CNRS. His research interest is static analysis of softwares, in order to prove correctness properties (e.g., absence of runtime errors, functional correctness, etc) in an automatic way.

Resources

• talk slide