Copenhagen Programming Language Seminar
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:
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 email@example.com with the word 'subscribe' as subject or in the body.
For more information about COPLAS, see http://www.coplas.org