Separation logic with monadic inductive definitions and implicit existentials

DOI10.1007/978-3-319-26529-2_5MaRDI QIDQ3460899zbMATH OpenOpenAlexFDO

Authors Makoto Tatsuta, Daisuke Kimura

Publication date 8 January 2016

Published in Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-26529-2_5

Mathematics Subject Classification ID

Logic in computer science (03B70) Data structures (68P05)

Recommendations

• The tree width of separation logic with recursive definitions
• Deciding entailments in inductive separation logic with tree automata
• Foundations for decision problems in separation logic with general inductive predicates
• Decision Procedure for Separation Logic with Inductive Definitions and Presburger Arithmetic
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science

Cited in

(11)

• Unifying decidable entailments in separation logic with inductive definitions
• Strong-separation logic
• The tree width of separation logic with recursive definitions
• Decidability for entailments of symbolic heaps with arrays
• Decision Procedure for Entailment of Symbolic Heaps with Arrays
• Logic Programming and Nonmonotonic Reasoning
• scientific article; zbMATH DE number 3321243 (Why is no real title available?)
• Completeness of cyclic proofs for symbolic heaps with inductive definitions
• Representation of Peano arithmetic in separation logic
• Beyond symbolic heaps: deciding separation logic with inductive definitions
• Encoding Peano arithmetic in a minimal fragment of separation logic

This page was built for publication: Separation logic with monadic inductive definitions and implicit existentials

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3460899)