BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Lightweight verification of separate compilation - Chung-Kil Hur\,
  Seoul National University
DTSTART:20180216T140000Z
DTEND:20180216T150000Z
UID:TALK98125@talks.cam.ac.uk
CONTACT:Victor Gomes
DESCRIPTION:Major compiler verification efforts\, such as the CompCert pro
 ject\, have traditionally simplified the verification problem by restricti
 ng attention to the correctness of whole-program compilation\, leaving ope
 n the question of how to verify the correctness of separate compilation. R
 ecently\, a number of sophisticated techniques have been proposed for prov
 ing more flexible\, compositional notions of compiler correctness\, but th
 ese approaches tend to be quite heavyweight compared to the simple “clos
 ed simulations” used in verifying whole-program compilation. Applying su
 ch techniques to a compiler like CompCert\, as Stewart et.al. have done\, 
 involves major changes and extensions to its original verification.\n\nIn 
 this talk\, I will show that if we aim somewhat lower—to prove correctne
 ss of separate compilation\, but only for a single compiler—we can drast
 ically simplify the proof effort. Toward this end\, we develop several lig
 htweight 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 demo
 nstrate the effectiveness of these techniques by applying them to CompCert
  2.4\, converting its verification of whole-program compilation into a ver
 ification of separate compilation in less than two person-months. This con
 version only required a small number of changes to the original proofs\, a
 nd uncovered two compiler bugs along the way. The result is SepCompCert\, 
 the first verification of separate compilation for the full CompCert compi
 ler.\n\nThis work was published at POPL 16 and more information can be fou
 nd at the following page.\n\nhttp://sf.snu.ac.kr/sepcompcert/
LOCATION:FW11
END:VEVENT
END:VCALENDAR