Date and Time: Thursday, 28 January 2010, 15:45 - 16:45

Location: HG 6.96

Speaker: Kees Huizing (FM)

Title: Expressivity of Pointer Formalisms

Abstract:

There are several formalisms for proving programs with pointers. We compared several of those, with the aim to select the one most appropriate for dealing with OO programs. We tried to show, in a limited setting without arithmetic, that Pointer Logic is more expressive than a variant of Separation Logic. There is a tantalizing hole in the proof that we would like to discuss at PROSE. At PROSE we will concisely explain the problem and wait for your solution.

Joint work with Mark Pustjens and Ruurd Kuiper