Fakultätskolloquium: "Graph-Based Static Analysis of Concurrent Pointer Programs", Dienstag, 01. August 2017, 16:00 Uhr, Raum WE5/05.003

Many software bugs can be traced back to the erroneous use of pointers, i.e., references to memory addresses. They constitute an essential concept in modern programming languages, and are used for implementing (dynamic) data structures like lists, trees etc., which are organised in the computer's memory as the so-called heap. Due to the resulting unbounded state spaces, pointer errors are hard to detect in sequential programs. Concurrency (in the form of threads or processes) raises additional challenges that are handled by current verification techniques only to a limited extent.
In this talk we introduce an abstraction framework for analysing pointer programs featuring dynamic data structures, recursive procedures, and concurrent threads. It uses a graph-based symbolic representation of sets of heaps and employs so-called hyperedge replacement grammars to describe both abstraction and concretisation operations on symbolic heaps. Modular reasoning is supported in the form of contracts with graphical pre- and postconditions that capture the net effect of a procedure's and thread's execution. In the latter case, contracts are enriched by so-called permissions that represent access rights to (parts of) the heap, which allows to check for race conditions and other concurrency issues. We also sketch a prototypical tool entitled that implements our approach and give some experimental verification results for several case studies involving list and tree data structures.

Thema: Graph-Based Static Analysis of Concurrent Pointer Programs
Referent: Dr. Thomas Noll (RWTH Aachen)
Zeit: Dienstag, 1. August 2017, 16:00 Uhr 
Ort: Raum WE5/05.003 (An der Weberei 5, 96047 Bamberg)