Automated Mutual Explicit Induction Proof in Separation Logic

TL;DR

This paper introduces an automated proof system for separation logic using mutual explicit induction, enabling automatic entailment proofs through a novel induction principle and implementation in a prototype prover.

Contribution

It presents a new mutual explicit induction proof technique for separation logic, integrating it into a deductive system with a prototype implementation.

Findings

Successfully proved a benchmark set of entailments

Demonstrated effectiveness on handcrafted and competition benchmarks

Enabled mutual induction in automated separation logic proofs

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.