Time: Wednesday 9.2.2005, 14:30
Place: Room A4-106, Fr. Bajersvej 7
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.