Static Analysis of Pointer Programs - Linking Graph Grammars and Separation Logic

This thesis presents a sound abstraction framework for the static analysis of pointer programs, which is able to handle (recursive) procedures as well as concurrency. The framework builds on a graph representation of the heap using so-called hypergraphs. In these graphs edges are labelled and can be connected to arbitrarily many vertices. Understanding edges between two vertices as pointers and the remaining edges as placeholders for parts of the heap, hypergraphs feature the necessary concepts for heap abstraction. More concretely, edge labels are used to specify the shape of the heap that is abstracted. Hyperedge replacement grammars formalise this mapping. That is, they define the data structures each of the labels represents. Concretisation and abstraction of heaps then directly correspond to forward and backward application of production rules of the hyperedge replacement grammar, respectively. The first part of the thesis lays the formal foundation for hypergraph-based heap representation and its concretisation and abstraction. Utilising this, an analysis approach for non-procedural pointer programs is presented. Additionally, we make requirements of hyperedge replacement grammars that are crucial for the soundness and termination of concretisation and abstraction. It is shown that each hyperedge replacement grammar can be transformed such that it satisfies these requirements. In the second part of the thesis, a bridge between hyperedge replacement grammars and the symbolic heap fragment of Separation Logic is built. In particular, a translation procedure between both formalisms is given and proven correct. Additionally, we provide the Separation Logic counterparts of the requirements determined in the preceding part and show that they are preserved by the translation. The relationship between Separation Logic and hyperedge replacement grammars inspired the extension to a framework that modularly handles procedures and fork-join-concurrency. That is, in the last part of the thesis we adopt the concept of contracts, i.e. pairs consisting of a pre- and a postcondition that capture the effect of a procedure or thread execution, to obtain procedure and thread modular analyses, respectively. In the latter case, we additionally introduce permissions to hypergraphs. They constitute a concept which is, similarly to contracts, well-understood for Separation Logic. Permissions provide transferable access grants to heap parts and enable the analysis of threads independently of each other. As a main contribution of the procedural and concurrent program analysis, a novel approach for automated derivation of procedure and (permission-enriched) thread contracts is presented