Anders Møller

BRICS, Department of Computer Science, Aarhus University, Denmark.

Time: Wednesday 9.2.2005, 14:30
Place: Room A4-106, Fr. Bajersvej 7

Verifying Programs That Manipulate Pointers

Reasoning about the correctness of programs that manipulate data structures using pointers is notoriously difficult: Destructive updating through pointers can make complex structures, the heap has an unbounded size, and data-structure invariants typically only hold at the beginning and end of operations. Correctness properties include absence of null pointer dereferences, dangling pointers, and leaking memory, but also more specialized requirements such as partial correctness of procedures.

This talk will give a brief overview of three approaches towards verifying programs that manipulate pointers: separation logic by Reynolds, O'Hearn, and others; parametric shape analysis by Sagiv, Reps, and Wilhelm; and pointer assertion logic by Møller and Schwartzbach.