Copenhagen Programming Language Seminar

Automatic Numeric Abstractions for Heap-Manipulating Programs

Stephen Magill
Carnegie Mellon; School of Computer Science

Thursday 19 February 2009, 13:00-14:00
The IT University, Rued Langgaards Vej 7, DK-2300 Room 2A.12


I will discuss an automatic method for going from heap-manipulating programs to numeric abstractions that is sound for both termination and safety reasoning.

The numeric abstractions are expressed as simple imperative programs over integer variables and have the property that termination and safety of the numeric program ensures termination and safety of the original, heap-manipulating program. The translation makes use of a shape analysis based on separation logic and has support for user-definend inductive data structures.

Scientific host:Lars Birkedal Administrative host: Annette Enggaard. All are welcome.
The Copenhagen Programming Language Seminar (COPLAS) is a collaboration between DIKU, ITU, KVL and RUC.
COPLAS is sponsored by the FIRST Graduate School.
To receive information about COPLAS talks by email, send a message to prog-lang-request@mail.it-c.dk with the word 'subscribe' as subject or in the body.

For more information about COPLAS, see http://www.coplas.org