Disproving inductive entailments in separation logic via base pair approximation

DOI10.1007/978-3-319-24312-2_20MaRDI QIDQ3455777zbMATH OpenOpenAlexFDO

Authors James Brotherston, Nikos Gorogiannis

Publication date 11 December 2015

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://eprints.mdx.ac.uk/19163/1/2015-tableaux.pdf

Mathematics Subject Classification ID

Logic in computer science (03B70) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• A decision procedure for satisfiability in separation logic with inductive predicates
• Automated cyclic entailment proofs in separation logic
• Deciding entailments in inductive separation logic with tree automata
• Frame inference for inductive entailment proofs in separation logic
• Automated mutual induction proof in separation logic

Cites work

• A decision procedure for satisfiability in separation logic with inductive predicates
• Automated verification of shape, size and bag properties via user-defined predicates in separation logic
• Automatic numeric abstractions for heap-manipulating programs
• Automating Inductive Proofs Using Theory Exploration
• Compositional shape analysis by means of bi-abduction
• Exponential Numbers
• Formalised Inductive Reasoning in the Logic of Bunched Implications
• Foundations for decision problems in separation logic with general inductive predicates
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
• Model checking for symbolic-heap separation logic with inductive predicates
• Permission accounting in separation logic
• Programming Languages and Systems
• The tree width of separation logic with recursive definitions
• Tractable Reasoning in a Fragment of Separation Logic

Cited in

(1)

• Entailment is undecidable for symbolic heap separation logic formulæ with non-established inductive rules

Describes a project that uses

Uses Software

• HipSpec
• Cyclist
• SLAyer
• VeriFast
• HIP
• Slide
• GitHub

This page was built for publication: Disproving inductive entailments in separation logic via base pair approximation

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