Fri 22 Jun 2018 14:25 - 14:50 at Grand Ballroom AB - Verification Chair(s): Adam Chlipala

Production compilers such as GCC and LLVM are large complex software systems, for which achieving a high level of reliability is hard. Although testing is an effective method for finding bugs, it alone cannot guarantee a high level of reliability. To provide a higher level of reliability, many approaches that examine compilers' internal logics have been proposed. However, none of them have been successfully applied to major optimizations of production compilers.

This paper presents Crellvm: a verified credible compilation framework for LLVM, which can be used as a systematic way of providing a high level of reliability for major optimizations in LLVM. Specifically, we augment an LLVM optimizer to generate translation results together with their correctness proofs, which can then be checked by a proof checker formally verified in Coq. As case studies, we applied our approach to two major optimizations of LLVM: register promotion mem2reg and global value numbering gvn, having found four new miscompilation bugs (two in each).

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