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

Displayed time zone: Eastern Time (US & Canada) change

14:00 - 15:40
VerificationPLDI Research Papers at Grand Ballroom AB
Chair(s): Adam Chlipala Massachusetts Institute of Technology, USA
14:00
25m
Talk
VeriPhy: Verified Controller Executables from Verified Cyber-Physical System Models
PLDI Research Papers
Brandon Bohrer , Yong Kiam Tan Carnegie Mellon University, USA, Stefan Mitsch Carnegie Mellon University, USA, Magnus O. Myreen Chalmers University of Technology, Sweden, André Platzer Carnegie Mellon University
Media Attached
14:25
25m
Talk
Crellvm: Verified Credible Compilation for LLVM
PLDI Research Papers
Jeehoon Kang Seoul National University, Yoonseung Kim Seoul National University (South Korea), Youngju Song Seoul National University, Juneyoung Lee Seoul National University, Sanghoon Park Seoul National University, South Korea, Mark Dongyeon Shin Seoul National University, South Korea, Yonghyun Kim Seoul National University, South Korea, Sungkeun Cho Seoul National University, South Korea, Joonwon Choi Massachusetts Institute of Technology, USA, Chung-Kil Hur Seoul National University, Kwangkeun Yi Seoul National University
Media Attached
14:50
25m
Talk
Certified Concurrent Abstraction Layers
PLDI Research Papers
Ronghui Gu Columbia University, Zhong Shao Yale University, Jieung Kim Yale University, USA, Xiongnan (Newman) Wu Yale University, Jérémie Koenig , Vilhelm Sjöberg Yale University, Hao Chen Yale University, David Costanzo Yale University, Tahina Ramananandro Microsoft Research, n.n.
Media Attached
15:15
25m
Talk
Modularity for Decidability of Deductive Verification with Applications to Distributed Systems
PLDI Research Papers
Marcelo Taube Tel Aviv University, Israel, Giuliano Losa University of California at Los Angeles, USA, Kenneth L. McMillan Microsoft Research, Oded Padon Tel Aviv University, Mooly Sagiv Tel Aviv University, Sharon Shoham Tel Aviv university, James R. Wilcox University of Washington, Doug Woos University of Washington
Media Attached