Publications
Detailed Information
Crellvm: Verified credible compilation for LLVM
Cited 0 time in
Web of Science
Cited 12 time in Scopus
- Authors
- Issue Date
- 2018-06
- Publisher
- Association for Computing Machinery
- Citation
- Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pp.631-645
- Abstract
- © 2018 Copyright held by the owner/author(s).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).
- Files in This Item:
- There are no files associated with this item.
Item View & Download Count
Items in S-Space are protected by copyright, with all rights reserved, unless otherwise indicated.