Wed 10 Jan 2018 13:40 - 14:05 at Bunker Hill - Verification I Chair(s): Zhong Shao

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.

Wed 10 Jan

13:40 - 15:20: Research Papers - Verification I at Bunker Hill
Chair(s): Zhong ShaoYale University
POPL-2018-papers13:40 - 14:05
Quang-Trung TaNational University of Singapore, Ton Chanh LeNational University of Singapore, Siau-Cheng KhooNational University of Singapore, Wei-Ngan ChinNational University of Singapore
POPL-2018-papers14:05 - 14:30
Christof LödingRWTH Aachen University, P. MadhusudanUniversity of Illinois at Urbana-Champaign, Lucas PeñaUniversity of Illinois at Urbana-Champaign
POPL-2018-papers14:30 - 14:55
Toby Cathcart BurnUniversity of Oxford, C.-H. Luke OngUniversity of Oxford, Steven RamsayUniversity of Bristol
POPL-2018-papers14:55 - 15:20
Hiroshi UnnoUniversity of Tsukuba, Yuki SatakeUniversity of Tsukuba, Tachio TerauchiWaseda University