Tractability of separation logic with inductive definitions: beyond lists

DOI10.4230/LIPICS.CONCUR.2017.37zbMATH Open1442.03013MaRDI QIDQ5111651FDOQ5111651

Authors: Taolue Chen, Fu Song, Zhilin Wu 

Publication date: 27 May 2020

Recommendations

• Tractable Reasoning in a Fragment of Separation Logic
• Foundations for decision problems in separation logic with general inductive predicates
• The tree width of separation logic with recursive definitions
• A decision procedure for satisfiability in separation logic with inductive predicates
• The effects of adding reachability predicates in propositional separation logic

zbMATH Keywords

satisfiabilityseparation logicentailmentinductive definitions

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Data structures (68P05) Logic in computer science (03B70)

Cites Work

• Deciding entailments in inductive separation logic with tree automata
• Programming Languages and Systems
• A decision procedure for separation logic in SMT
• Automated verification of shape, size and bag properties via user-defined predicates in separation logic
• Title not available (Why is that?)
• Tractable Reasoning in a Fragment of Separation Logic
• On the almighty wand
• Title not available (Why is that?)
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
• The tree width of separation logic with recursive definitions
• Compositional entailment checking for a fragment of separation logic
• A complete decision procedure for linearly compositional separation logic with data constraints
• On automated lemma generation for separation logic with inductive definitions
• Satisfiability modulo heap-based programs
• A decision procedure for satisfiability in separation logic with inductive predicates
• Automated cyclic entailment proofs in separation logic
• Decision Procedure for Separation Logic with Inductive Definitions and Presburger Arithmetic
• Foundations for decision problems in separation logic with general inductive predicates
• Biabduction (and related problems) in array separation logic
• Satisfiability of compositional separation logic with tree predicates and data constraints
• Model checking for symbolic-heap separation logic with inductive predicates
• Expressive completeness of separation logic with two variables and no separating conjunction

Cited In (8)

• The effects of adding reachability predicates in propositional separation logic
• Foundations for decision problems in separation logic with general inductive predicates
• Unifying decidable entailments in separation logic with inductive definitions
• The tree width of separation logic with recursive definitions
• An efficient cyclic entailment procedure in a fragment of separation logic
• Decision Procedure for Separation Logic with Inductive Definitions and Presburger Arithmetic
• Separation logic with linearly compositional inductive predicates and set data constraints
• On the complexity of pointer arithmetic in separation logic

Uses Software

• HIP
• Infer
• Slide
• SeLoger

This page was built for publication: Tractability of separation logic with inductive definitions: beyond lists

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