Enhancing Inductive Entailment Proofs in Separation Logic with Lemma Synthesis

TL;DR

This paper introduces an automated lemma synthesis approach to improve inductive entailment proofs in separation logic, enabling more expressive and automated reasoning for complex inductive proofs.

Contribution

It presents a novel mechanism for automatic lemma proof and application, supporting universal guards, unknown predicates, and enhancing inductive reasoning and theorem exploration.

Findings

Successfully integrated into an existing verification system.

Automatically synthesizes lemmas for complex inductive proofs.

Improves reasoning capabilities on non-trivial proofs.

Abstract

This paper presents an approach to lemma synthesis to support advanced inductive entailment procedures based on separation logic. We first propose a mechanism where lemmas are automatically proven and systematically applied. The lemmas may include universal guard and/or unknown predicate. While the former is critical for expressivity, the latter is essential for supporting relationships between multiple predicates. We further introduce lemma synthesis to support (i) automated inductive reasoning together with frame inference and (ii) theorem exploration. For (i) we automatically discover and prove auxiliary lemmas during an inductive proof; and for (ii) we automatically generate a useful set of lemmas to relate user-defined or system-generated predicates. We have implemented our proposed approach into an existing verification system and tested its capability in inductive reasoning and theorem exploration. The experimental results show that the enhanced system can automatically synthesize useful lemmas to facilitate reasoning on a broad range of non-trivial inductive proofs.