References & Citations
Computer Science > Programming Languages
Title: Enhancing Inductive Entailment Proofs in Separation Logic with Lemma Synthesis
(Submitted on 17 Oct 2017 (v1), last revised 12 May 2018 (this version, v2))
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.
Submission history
From: Quang Loc Le [view email][v1] Tue, 17 Oct 2017 22:13:25 GMT (704kb)
[v2] Sat, 12 May 2018 10:10:29 GMT (158kb)
Link back to: arXiv, form interface, contact.