DIKU ITU KVL

Copenhagen Programming Language Seminar

COPLAS Talk

Beyond Reachability: Shape Abstraction in the Presence of Pointer Arithmetic

Hongseok Yang,
Seoul National University

Thursday, August 10th, 13:00-14:00
IT University of Copenhagen, Rued Langgaards Vej 7, Auditorium 3

Abstract:

Previous shape analysis algorithms assume that the heap can be characterized in terms of reachability, that it is composed of discrete nodes that can be accessed only via access paths built from variables and field names. This assumption is violated by pointer arithmetic.
In this talk I will describe a shape analysis that works in the presence of pointer arithmetic. The abstract domain uses formulae in separation logic, leveraging that logic's non-reliance on reachability assumptions for its soundness. The analysis has been applied to verify series of programs for dynamic memory management.

This is joint work with Dino Distefano, Peter O'Hearn and Cristiano Calcagno.

Scientific host: Lars Birkedal. Administrative host: Camilla Jensen. All are welcome.
The Copenhagen Programming Language Seminar (COPLAS) is a collaboration between DIKU, ITU and KVL.
COPLAS is sponsored by 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