Copenhagen Programming Language Seminar
Shape analyses are unique in that they can capture detailed aliasing and structural information that is typically beyond the ability of other static program analyses. To do so, they rely on specialized data structure descriptions to build precise heap abstractions. A key component of shape analyses that enable such precision is a partial concretization operation on abstract memories (i.e., materialization).
In many respects, inductively-defined data structure specifications are a natural fit for shape analysis. First, we observe that they often resemble data structure invariant checkers used by program developers for testing or dynamic analysis. Second, they yield a straightforward materialization operation, that is, the unfolding of inductive definitions.
In this talk, we discuss an automated shape analysis parameterized by such developer-supplied inductive checkers. We focus on the challenges in designing such a parametric memory abstraction, which centers on abstractions for local invariants at intermediate program points (i.e., when the global data structure invariant holds only partially). In particular, we propose a generic unfolding (i.e., materialization) operation built on a type pre-analysis on the developer-supplied checkers. Such a mechanism is particularly important for data structures with back pointers, such a doubly-linked lists and trees with parent pointers.
Scientific host: Carsten
Schürmann . 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 email@example.com with the word 'subscribe' as subject or in the body.
For more information about COPLAS, see http://www.coplas.org