Analysis and Verification of Pointer Programs

Seminar in Theoretical CS, Winter Semester 2016/17

News

  • 23.06.2016: we are online

Deadlines

20.10.2016, 14:00 Introduction at seminar room of i2 (building E1, room 4201b)
21.11.2016 Detailed outline of report due
12.12.2016 Seminar report due
09.01.2017 Presentation slides due
19.01.2017, 14:00-17:00 Seminar at seminar room of i2 (building E1, room 4201b)

Overview

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 realising (dynamic) data structures like lists, trees etc., which are organised in the computer’s memory as a so-called heap. Pointers are also abundantly present in object-oriented software such as Java collections, albeit in the somewhat implicit form of object references. Pointer-handling operations occur in device drivers, operating systems, and all kinds of application codes including those implementing safety-critical systems. The analysis of such software is a highly demanding and important task, as memory leaks, dereferencing null pointers or the accidental invalidation of data structures can cause great damage especially when software reliability is at stake. Moreover, the increasing presence of concurrency in modern computing raises additional problems such as the non-synchronised access to memory areas, which can entail so-called data races. Even worse, the formal analysis of concurrent software poses additional challenges caused by the non-deterministic execution order (interleaving) between different strands of concurrent activities.

In consequence, the complexity of state spaces arising from dynamic data structures, recursive method or procedure calls, and dynamic creation of and interleaving between concurrent threads imposes challenges which cannot be handled by standard verification algorithms such as finite-state model checking. This problem has been a topic of continuous research interest since the early 1970s. A common approach are abstraction techniques that employ symbolic representations of sets of program states using suitable formalisms. Various such formalisms have been considered for this purpose, which can be distinguished with regard to their expressiveness, precision, efficiency, and automatability. The goal of this seminar is to study a particularly successful logical approach, namely, Separation Logic. Its importance is witnessed by the 2016 Gödel Prize, which was awarded to Stephen Brookes and Peter W. O’Hearn for their invention of Concurrent Separation Logic.

Prerequisites

Basic knowledge in the following areas is expected:

  • Formal languages and automata theory
  • Mathematical logic
  • Previous knowledge in semantics of programming languages, program analysis, model checking and/or concurrency theory is helpful but not mandatory

Topics

(The “B” and “M” tags respectively refer to topics on BSc and MSc level.)

  1. B: Local Shape Analysis
  2. B: Compositional Shape Analysis
  3. B: Cyclic Entailment Proofs
  4. B/M: Arithmetic Strengthening for Shape Analysis
  5. B/M: Amortised Resource Analysis
  6. M: Concurrent Separation Logic

Additional Material

Registration

Registration to the seminar is handled between June 24 and July 10, 2016, via the central online form. Later applications will not be considered.

Contact

Thomas Noll <noll at cs.rwth-aachen.de>