Symbolic Representations of Dynamic Data Structures in Program Analysis

Formal verification, shape analysis, finite automata, tree automata, separation logic, monadic second-order logic, decidability

In this habilitation thesis, we discuss the problem of verification of programs with pointers and dynamic memory allocation. One of the main components needed in verification of these programs is a suitable representation of a (potentially infinite) set of memory configurations often called shape graphs. Shape graphs are in fact unrestricted oriented graphs, and, moreover, we have to work with infinite sets of these objects. A suitable symbolic model of memory configurations must satisfy the following properties: First, it must describe in a finite way an infinite number of shape graphs. Second, it must allow an execution of program statements on the level of the symbolic model. And finally, some acceleration technique must exists to guarantee a termination of the execution on the level of the used symbolic model. In this thesis, we discuss various types of automata and logics as natural tools to represent infinite sets of objects, which can be used as symbolic models of shape graphs. In the area of automata, we describe use of finite automata, tree automata, forest automata, counter automata, and we discuss also the concept of graph automata. In the area of logics, we concentrate mostly on monadic second-order logic and separation logic. The main part of this thesis is a collection of original research papers, where the author of this thesis is the key contributor.