1. Forum
  2. Usenet
  3. COMP.DOC.TECHREPORTS

  • AIB 2015-12: Tree-like Grammars and Separation Logic

    From =?UTF-8?Q?Thomas_Str=c3=b6der?=@21:1/5 to All on Wed Sep 23 09:14:43 2015
    The following technical report is available from http://aib.informatik.rwth-aachen.de:

    Tree-like Grammars and Separation Logic
    Christoph Matheja, Christina Jansen, and Thomas Noll
    AIB 2015-12

    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.

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)