Computer Science Graduate Seminar: Static Analysis of Pointer Programs using Graph Grammar-Guided Abstraction

 

Thursday, October 19, 2017, 2:00pm

Location: 2356|053.2a (B-IT room, E2)

Speaker: Dipl.-Inform. Christina Jansen

Abstract:

With growing size and complexity of software, automated verification techniques become more and more essential. Many software projects employ object-oriented languages, which introduce new challenges to formal reasoning. In particular, the analysis of programs that use pointers to implement dynamic data structures and that enable destructive updates is a highly demanding and important task, because memory leaks, dereferencing null pointers or functional errors can cause great damage especially when software reliability is of great importance. As objects can be created at runtime, dynamic data structures induce potentially infinite state spaces, which cannot be handled by standard verification algorithms. A common way to address these problems is to apply abstraction techniques that yield finite representations for such data structures. In this talk, I will present a graph-based abstract interpretation framework for pointer programs. It employs a natural graph-based model of heap structures where vertices are interpreted as heap objects while labelled edges (i.e., pairs of vertices) visualise references between the objects. Operational semantics of programs are given by a transition system whose states are these heap graphs, while the transitions correspond to graph transformations. To define abstractions a generalisation of graphs, so-called hypergraphs, is utilised. Hypergraphs feature hyperedges, which connect an arbitrary number of vertices. The key idea for abstraction is to employ labelled hyperedges to represent parts of a heap. The edge label indicates which heap shape or data structure is represented, e.g., a singly- or doubly-linked list of arbitrary length. Hyperedge replacement grammars formalise the mapping from labels to heap shapes by interpreting the former as nonterminal symbols. Doing so, abstraction and concretisation can be represented elegantly: The production rules of the graph grammar reflect the data structures that occur in the program, such as lists, trees, lists of trees, etc. Their forward application, i.e., replacing a nonterminal-labelled edge with a hypergraph, yields a concretisation of the abstract heap fragment. A backward application, that is, the replacement of a graph by a hyperedge, represents an abstraction step that condenses a subgraph of the heap into a single labelled edge. In the course of the talk we extend the abstract interpretation approach to concurrent pointer programs. This extension still employs graph grammars to abstract the data structures occurring during program execution. For dealing with the program's control flow, however, modular reasoning in form of contracts on the level of threads is used.

The Computer Science lecturers invite interested people to join.