Thursday, January 21, 2016
Speaker: Christoph Matheja
Venue: TU Wien
Separation Logic with inductive predicate definitions (SL) and hyperedge
replacement grammars (HRG) are established formalisms to describe the
abstract shape of data structures maintained by heap-manipulating programs.
Fragments of both formalisms are known to coincide, and neither the
entailment problem for SL nor its counterpart for HRGs, the inclusion
problem, are decidable in general.
We introduce tree-like grammars (TLG), a fragment of HRGs with a
decidable inclusion problem.
By the correspondence between HRGs and SL, we simultaneously obtain an
equivalent SL fragment (SLTL) featuring some remarkable properties
including a decidable entailment problem.