Automated Lemma Synthesis in Symbolic-Heap Separation Logic

Watch a 24-minute conference presentation from POPL 2018 exploring an innovative framework for automated lemma synthesis in symbolic-heap separation logic. Learn how researchers from the National University of Singapore developed a system to automatically discover supporting lemmas for proving entailments containing inductive heap predicates. Understand the framework's key components including mathematical induction and template-based constraint solving, which help verify programs manipulating complex data structures like linked lists, trees and graphs. Discover how the system identifies lemma templates from heap structures, establishes unknown relations between variables, conducts structural induction proofs to generate constraints, and solves these constraints to derive actual lemmas. See experimental results demonstrating how this lemma-synthesis-assisted prover successfully handles entailments that previous techniques could not process, advancing automated reasoning capabilities for complex inductive heap predicates.