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:20170929T130000Z
DTEND:20170929T140000Z
UID:TALK75431@talks.cam.ac.uk
CONTACT:Peter Sewell
DESCRIPTION:Major compiler verification efforts\, such as the CompCert pro
 ject\,\nhave traditionally simplified the verification problem by restrict
 ing\nattention to the correctness of whole-program compilation\, leaving\n
 open the question of how to verify the correctness of separate\ncompilatio
 n. Recently\, a number of sophisticated techniques have been\nproposed for
  proving more flexible\, compositional notions of compiler\ncorrectness\, 
 but these approaches tend to be quite heavyweight\ncompared to the simple 
 "closed simulations" used in verifying\nwhole-program compilation. Applyin
 g such techniques to a compiler like\nCompCert\, as Stewart et.al. have do
 ne\, involves major changes and\nextensions to its original verification.\
 n\nIn this talk\, I will show that if we aim somewhat lower—to prove\nco
 rrectness of separate compilation\, but only for a single compiler—we\nc
 an drastically simplify the proof effort. Toward this end\, we develop\nse
 veral lightweight techniques that recast the compositional\nverification p
 roblem in terms of whole-program compilation\, thereby\nenabling us to lar
 gely reuse the closed-simulation proofs from\nexisting compiler verificati
 ons. We demonstrate the effectiveness of\nthese techniques by applying the
 m to CompCert 2.4\, converting its\nverification of whole-program compilat
 ion into a verification of\nseparate compilation in less than two person-m
 onths. This conversion\nonly required a small number of changes to the ori
 ginal proofs\, and\nuncovered two compiler bugs along the way. The result 
 is SepCompCert\,\nthe first verification of separate compilation for the f
 ull CompCert\ncompiler.\n\nThis work was published at POPL 16 and more inf
 ormation can be\nfound at the following page.\n\nhttp://sf.snu.ac.kr/sepco
 mpcert/
LOCATION:FW26
END:VEVENT
END:VCALENDAR