Time: Wednesday 9.2.2005, 14:30
Place: Room A4-106, Fr. Bajersvej 7
Reasoning about the correctness of programs that manipulate data structures
is notoriously difficult: Destructive updating through pointers can make
structures, the heap has an unbounded size, and data-structure invariants
hold at the beginning and end of operations. Correctness properties include
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.