Disproving Inductive Entailments in Separation Logic via Base Pair Approximation

DOI10.1007/978-3-319-24312-2_20zbMath1471.03062OpenAlexW2241234471MaRDI QIDQ3455777

Nikos Gorogiannis, James Brotherston

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)

Uses Software

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

Cites Work

• Automated verification of shape, size and bag properties via user-defined predicates in separation logic
• Model checking for symbolic-heap separation logic with inductive predicates
• Tractable Reasoning in a Fragment of Separation Logic
• Formalised Inductive Reasoning in the Logic of Bunched Implications
• A decision procedure for satisfiability in separation logic with inductive predicates
• Exponential Numbers
• The Tree Width of Separation Logic with Recursive Definitions
• Automating Inductive Proofs Using Theory Exploration
• Automatic numeric abstractions for heap-manipulating programs
• Permission accounting in separation logic
• Compositional Shape Analysis by Means of Bi-Abduction
• Foundations for Decision Problems in Separation Logic with General Inductive Predicates
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
• Programming Languages and Systems

This page was built for publication: Disproving Inductive Entailments in Separation Logic via Base Pair Approximation