PLDI 2018 (series) / PLDI Research Papers /
Modularity for Decidability of Deductive Verification with Applications to Distributed Systems
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.
Conference DayFri 22 JunDisplayed time zone: Eastern Time (US & Canada) change
Conference Day
Fri 22 JunDisplayed time zone: Eastern Time (US & Canada) change
14:00 - 15:40 | VerificationPLDI Research Papers at Grand Ballroom AB Chair(s): Adam ChlipalaMassachusetts Institute of Technology, USA | ||
14:00 25mTalk | VeriPhy: Verified Controller Executables from Verified Cyber-Physical System Models PLDI Research Papers 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 | ||
14:25 25mTalk | Crellvm: Verified Credible Compilation for LLVM PLDI Research Papers 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 | ||
14:50 25mTalk | Certified Concurrent Abstraction Layers PLDI Research Papers Ronghui GuColumbia University, Zhong ShaoYale University, Jieung KimYale University, USA, Xiongnan (Newman) WuYale University, Jérémie Koenig, Vilhelm SjöbergYale University, Hao ChenYale University, David CostanzoYale University, Tahina RamananandroMicrosoft Research, n.n. Media Attached | ||
15:15 25mTalk | Modularity for Decidability of Deductive Verification with Applications to Distributed Systems PLDI Research Papers 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 | ||