Paper Info
Title
Crellvm: verified credible compilation for LLVM.
Abstract
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).
Year
DOI
Venue
2018
10.1145/3192366.3192377
PLDI
Keywords
Field
DocType
Coq, LLVM, compiler verification, credible compilation, relational Hoare logic, translation validation
Global value numbering,Correctness proofs,Programming language,Compiler verification,Computer science,Effective method,Automated proof checking,Compiler,Software system
Conference
Volume
Issue
ISSN
53
4
0362-1340
ISBN
Citations 
PageRank 
978-1-4503-5698-5
2
0.37
References 
Authors
21
11
Name
Order
Citations
PageRank
Jeehoon Kang121.72
Yoonseung Kim2191.35
Youngju Song3111.24
Juneyoung Lee4111.92
Sanghoon Park591.97
Mark Dongyeon Shin620.37
Yonghyun Kim753.10
Sung-Keun Cho8111.56
Joonwon Choi9111.57
Chung-Kil Hur1025417.07
Kwangkeun Yi1161244.24