Automated Mutual Explicit Induction Proof in Separation Logic

2016/09/04 by Ta, Quang-Trung, Le, Ton Chanh, Khoo, Siau-Cheng +1 · 2 citations
#FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Programming Languages (cs.PL)

paper · doi:10.48550/arxiv.1609.00919

Abstract

We present a sequent-based deductive system for automatically proving entailments in separation logic by using mathematical induction. Our technique, called mutual explicit induction proof, is an instance of Noetherian induction. Specifically, we propose a novel induction principle on a well-founded relation of separation logic model and follow the explicit induction methods to implement this principle as inference rules, so that it can be easily integrated into a deductive system. We also support mutual induction, a natural feature of implicit induction, where the goal entailment and other entailments derived during the proof search can be used as hypotheses to prove each other. We have implemented a prototype prover and evaluated it on a benchmark of handcrafted entailments as well as benchmarks from a separation logic competition.

Cited by

• Stellis: A Strategy Language for Purifying Separation Logic Entailments
• Separating the Wheat from the Chaff: Understanding (In-)Completeness of Proof Mechanisms for Separation Logic with Inductive Definitions

Related

• An Entailment Checker for Separation Logic with Inductive Definitions
• An Entailment Checker for Separation Logic with Inductive Definitions
• Enhancing Inductive Entailment Proofs in Separation Logic with Lemma Synthesis
• A Proof Procedure For Separation Logic With Inductive Definitions and Theory Reasoning
• A Decision Procedure for Guarded Separation Logic: Complete Entailment Checking for Separation Logic with Inductive Definitions