Automated mutual induction proof in separation logic

DOI10.1007/s00165-018-0471-5zbMath1425.68382OpenAlexW2897577612WikidataQ129100621 ScholiaQ129100621MaRDI QIDQ2414251

Wei-Ngan Chin, Quang-Trung Ta, Ton Chanh Le, Siau-Cheng Khoo

Publication date: 10 May 2019

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00165-018-0471-5

zbMATH Keywords

mathematical inductionseparation logicentailment provingmutual induction

Mathematics Subject Classification ID

Related Items (4)

Generalized arrays for Stainless frames ⋮ An efficient cyclic entailment procedure in a fragment of separation logic ⋮ Unifying decidable entailments in separation logic with inductive definitions ⋮ A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions

Uses Software

• z3
• SLAyer
• HIP
• Cyclist
• Slide

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Automated verification of shape, size and bag properties via user-defined predicates in separation logic
• Quantitative separation logic and programs with lists
• Automated mutual explicit induction proof in separation logic
• Compositional Entailment Checking for a Fragment of Separation Logic
• Model checking for symbolic-heap separation logic with inductive predicates
• Separation Logic Modulo Theories
• Matching, unification and complexity
• Deciding Entailments in Inductive Separation Logic with Tree Automata
• On Automated Lemma Generation for Separation Logic with Inductive Definitions
• Enhancing Program Verification with Lemmas
• Formalised Inductive Reasoning in the Logic of Bunched Implications
• The Tree Width of Separation Logic with Recursive Definitions
• Automated Cyclic Entailment Proofs in Separation Logic
• Automated Verification of Shape and Size Properties Via Separation Logic
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
• Programming Languages and Systems

This page was built for publication: Automated mutual induction proof in separation logic