Write a Blog >>
Wed 20 Jan 2016 14:45 - 15:10 at Grand Bay South - Track 2: Correct Compilation Chair(s): Jens Palsberg

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 paper, we 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 v2.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.

Poster (poster.pdf)4.44MiB

Wed 20 Jan

Displayed time zone: Guadalajara, Mexico City, Monterrey change

14:20 - 16:00
Track 2: Correct CompilationResearch Papers at Grand Bay South
Chair(s): Jens Palsberg University of California, Los Angeles
14:20
25m
Talk
Fully-Abstract Compilation by Approximate Back-Translation
Research Papers
Dominique Devriese iMinds - Distrinet, KU Leuven, Marco Patrignani KU Leuven, Frank Piessens iMinds - Distrinet, KU Leuven
Pre-print Media Attached
14:45
25m
Talk
Lightweight Verification of Separate Compilation
Research Papers
Jeehoon Kang Seoul National University, Yoonseung Kim Seoul National University (South Korea), Chung-Kil Hur Seoul National University, Derek Dreyer MPI-SWS, Viktor Vafeiadis MPI-SWS, Germany
Media Attached File Attached
15:10
25m
Talk
From MinX to MinC: Semantics-Driven Decompilation of Recursive Datatypes
Research Papers
Ed Robbins Kent, Andy King Kent, Tom Schrijvers KU Leuven
Media Attached
15:35
25m
Talk
Sound Type-dependent Syntactic Language Extension
Research Papers
Florian Lorenzen TU Berlin, Sebastian Erdweg TU Darmstadt, Germany
Pre-print Media Attached File Attached