COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. |

University of Cambridge > Talks.cam > Logic and Semantics Seminar (Computer Laboratory) > Lightweight verification of separate compilation

## Lightweight verification of separate compilationAdd to your list(s) Download to your calendar using vCal - Chung-Kil Hur, Seoul National University
- Friday 29 September 2017, 14:00-15:00
- FW26.
If you have a question about this talk, please contact Peter Sewell. NB: rescheduled from 2017/09/22 Major compiler verification efforts, such as the CompCert project, have traditionally simplified the verification problem by restricting attention to the correctness of whole-program compilation, leaving open the question of how to verify the correctness of separate compilation. Recently, a number of sophisticated techniques have been proposed for proving more flexible, compositional notions of compiler correctness, but these approaches tend to be quite heavyweight compared to the simple “closed simulations” used in verifying whole-program compilation. Applying such techniques to a compiler like CompCert, as Stewart et.al. have done, involves major changes and extensions to its original verification. In this talk, I will show that if we aim somewhat lowerâ€”to prove correctness of separate compilation, but only for a single compilerâ€”we can drastically simplify the proof effort. Toward this end, we develop several lightweight techniques that recast the compositional verification problem in terms of whole-program compilation, thereby enabling us to largely reuse the closed-simulation proofs from existing compiler verifications. We demonstrate the effectiveness of these techniques by applying them to CompCert 2.4, converting its verification of whole-program compilation into a verification of separate compilation in less than two person-months. This conversion only required a small number of changes to the original proofs, and uncovered two compiler bugs along the way. The result is SepCompCert, the first verification of separate compilation for the full CompCert compiler. This work was published at POPL 16 and more information can be found at the following page. http://sf.snu.ac.kr/sepcompcert/ This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series. ## This talk is included in these lists:- All Talks (aka the CURE list)
- Computer Laboratory talks
- Computing and Mathematics
- FW26
- Logic and Semantics Seminar (Computer Laboratory)
- School of Technology
Note that ex-directory lists are not shown. |
## Other listsClare Hall Talks Seven Types of Forgetting Talks at Centre of Molecular Materials for Photonics and Electronics (CMMPE)## Other talksCambridge Parasitic and Neglected Diseases Network Meeting Modular Algorithm Analysis Applications and extensions. Short Course: Higher order regularisation in imaging - Lecture 3 Dr. Ulrich Schwarz-Linek - Title to be Confirmed Machine Learning for Sounds How Quantum Physics Democratised Music: A Meditation on Physics and Technology |