Inria Paris, France
Inria Paris, France
This course will cover several families of abstract domains to describe properties of memory states. First, we will discuss the formalisation of concrete memory states and common target properties such as basic memory safety, the preservation of structural invariants, and more advanced functional properties. Second, we will point out the main challenges for the design of static analyses that compute properties over memory states. Then, we will study several kinds of abstractions for memory properties. In particular, we will cover dynamic abstractions for arrays and inductive data-structures, that rely on separation logic. In both cases, we will use summary predicates, that describe memory regions of unbounded size. We will formalise a subset of separation logic and show a machine representation for this fragment. We will also cover the design of abstract operators and their combination in order to build a static analysis. Finally, we will extend this analysis with a combined abstract domain that expresses properties about both the shape of the data-structures and the numeric values stored in them.