Synthesizing data structure grammars from separation logic predicates and vice versa

Speaker

Florian Göbe

Title Synthesizing data structure grammars from separation logic predicates and vice versa
When 03.09.2012, 12:30
Where Seminarroom I2 (!)
Abstract Hyperedge replacement grammars (HRGs) are a convenient way to reason about dynamic data structures modelled as hypergraphs. On the one hand HRGs are suitable to define languages of data structure instances. On the other hand they form a convenient tool to condense those parts of the memory that the considered program does currently not operate on using hyperedges labelled with non>terminal symbols, achieving a finite abstraction of the infinite state space. Separation logic (SL), which is an extension of Hoare logic, is another approach to describe the heap by assertions with recursive predicates. In this talk the analogies and differences of the two concepts will be analysed and a sound translation method to synthesize grammars from SL formulae and vice versa will be presented.
Slides