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

We give foundational results that explain the efficacy of heuristics used for dealing with quantified formulas and recursive definitions. We develop a framework for first order logic (FOL) over an uninterpreted combination of background theories. Our central technical result is that systematic term instantiation is \emph{complete} for a fragment of FOL that we call safe. Coupled with the fact that unfolding recursive definitions is essentially term instantiation and with the observation that heap verification engines generate verification conditions in the safe fragment explains the efficacy of verification engines like natural proofs that resort to such heuristics. Furthermore, we study recursive definitions with least fixpoint semantics and show that though they are not amenable to complete procedures, we can systematically introduce induction principles that in practice bridge the divide between FOL and FOL with recursive definitions.

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