Fri 22 Jun 2018 15:15 - 15:40 at Grand Ballroom AB - Verification Chair(s): Adam Chlipala

Proof automation can substantially increase productivity in formal verification of complex systems. However, unpredictablility of automated provers in handling quantified formulas presents a major hurdle to usability of these tools. We propose to solve this problem not by improving the provers, but by using a modular proof methodology that allows us to produce \emph{decidable} verification conditions. Decidability greatly improves predictability of proof automation, resulting in a more practical verification approach. We apply this methodology to develop verified implementations of distributed protocols, demonstrating its effectiveness.

Fri 22 Jun

pldi-2018-papers
14:00 - 15:40: PLDI Research Papers - Verification at Grand Ballroom AB
Chair(s): Adam ChlipalaMassachusetts Institute of Technology, USA
pldi-2018-papers14:00 - 14:25
Talk
Brandon Bohrer, Yong Kiam TanCarnegie Mellon University, USA, Stefan MitschCarnegie Mellon University, USA, Magnus O. MyreenChalmers University of Technology, Sweden, André PlatzerCarnegie Mellon University
Media Attached
pldi-2018-papers14:25 - 14:50
Talk
Jeehoon KangSeoul National University, Yoonseung KimSeoul National University (South Korea), Youngju SongSeoul National University, Juneyoung LeeSeoul National University, Sanghoon ParkSeoul National University, South Korea, Mark Dongyeon ShinSeoul National University, South Korea, Yonghyun KimSeoul National University, South Korea, Sungkeun ChoSeoul National University, South Korea, Joonwon ChoiMassachusetts Institute of Technology, USA, Chung-Kil HurSeoul National University, Kwangkeun YiSeoul National University
Media Attached
pldi-2018-papers14:50 - 15:15
Talk
Ronghui GuColumbia University, Zhong ShaoYale University, Jieung KimYale University, USA, Xiongnan (Newman) WuYale University, Jérémie Koenig, Vilhelm SjobergYale University, Hao ChenYale University, David CostanzoYale University, Tahina RamananandroMicrosoft Research, n.n.
Media Attached
pldi-2018-papers15:15 - 15:40
Talk
Marcelo TaubeTel Aviv University, Israel, Giuliano LosaUniversity of California at Los Angeles, USA, Kenneth L. McMillanMicrosoft Research, Oded PadonTel Aviv University, Mooly SagivTel Aviv University, Sharon ShohamTel Aviv university, James R. WilcoxUniversity of Washington, Doug WoosUniversity of Washington
Media Attached