The symbolic-heap fragment of separation logic has been actively developed and applied in verifying the memory-safety of imperative programs in recent years. At the current stage, one of its biggest challenges is how to effectively prove entailments containing inductive heap predicates. These entailments are usually proof obligations generated during the verification of programs manipulating complex data structures such as variants of linked lists, trees, or graphs.

To assist in proving such entailments (i.e. with inductive heap predicates in symbolic-heap separation logic), this paper introduces a lemma synthesis framework, which automatically discovers lemmas to serve as eureka steps in their proofs. Mathematical induction and template-based constraint solving are two pillars of our framework. To derive the supporting lemmas for a given entailment, the framework firstly identifies several possible lemma templates from the entailment’s heap structure, then sets up unknown relations among the variables of each template and conducts structural induction proof to generate constraints about these relations, and finally solves these constraints to find out the unknown relations’ actual definitions, thus discovers the lemmas. We have integrated this framework in a prototype separation logic prover and experiment it on various entailment benchmarks. The experimental results show that our lemma-synthesis-assisted prover can prove many entailments while the existing techniques cannot. This paper opens up opportunities to apply reasoning about inductive heap predicates into practical program verification.