SPLASH 2020
Sun 15 - Sat 21 November 2020 Online Conference
Wed 18 Nov 2020 18:00 - 18:20 at SPLASH-I - W-6 Chair(s): Anitha Gollamudi, Hans-J. Boehm
Thu 19 Nov 2020 06:00 - 06:20 at SPLASH-I - W-6 Chair(s): John Wickerson, Jan Vitek

<p>
We present CompCertELF, the first extension to CompCert that
supports verified compilation from C programs all the way to a
standard binary file format, i.e., the ELF object format.
Previous work on Stack-Aware CompCert provides a verified
compilation chain from C programs to assembly programs with a
realistic machine memory model. We build CompCertELF by
modifying and extending this compilation chain with a verified
assembler which further transforms assembly programs into ELF
object files.
</p>

<p>
CompCert supports large-scale verification via verified separate
compilation: C modules can be written and compiled separately,
and then linked together to get a target program that refines the
semantics of the program linked from the source modules.
However, verified separate compilation in CompCert only works for
compilation to assembly programs, not to object files. For the
latter, the main difficulty is to bridge the two different views
of linking: one for CompCert's programs that allows arbitrary
shuffling of global definitions by linking and the other for
object files that treats blocks of encoded definitions as
indivisible units.
</p>

<p>
We propose a lightweight approach that solves the above problem
without any modification to CompCert's framework for verified
separate compilation: by introducing a notion of syntactical
equivalence between programs and proving the commutativity
between syntactical equivalence and the two different kinds of
linking, we are able to transit from the more abstract linking
operation in CompCert to the more concrete one for ELF object
files. By applying this approach to CompCertELF, we obtain the
first compiler that supports verified separate compilation of C
programs into ELF object files.
</p>

Wed 18 Nov
Times are displayed in time zone: Central Time (US & Canada) change

17:00 - 18:20: W-6OOPSLA at SPLASH-I +12h
Chair(s): Anitha GollamudiHarvard University, Hans-J. BoehmGoogle
17:00 - 17:20
Talk
Programming with a Read-Eval-Synth Loop
OOPSLA
Hila PelegUniversity of California at San Diego, Roi GabayTechnion, Shachar ItzhakyTechnion, Eran YahavTechnion
Link to publication DOI Media Attached
17:20 - 17:40
Talk
Sound Garbage Collection for C using Pointer Provenance
OOPSLA
Subarno BanerjeeUniversity of Michigan, David DevecseryGeorgia Institute of Technology, Peter M. ChenUniversity of Michigan, Satish NarayanasamyUniversity of Michigan
Link to publication DOI Media Attached
17:40 - 18:00
Talk
Semiring Optimizations: Dynamic Elision of Expressions with Identity and Absorbing Elements
OOPSLA
Guilherme Vieira LeobasFederal University of Minas Gerais, Fernando Magno Quintão PereiraFederal University of Minas Gerais
Link to publication DOI Pre-print Media Attached
18:00 - 18:20
Talk
CompCertELF: Verified Separate Compilation of C Programs into ELF Object Files
OOPSLA
Yuting WangShanghai Jiao Tong University, Xiangzhe XuNanjing University, Pierre WilkeCentraleSupélec, Zhong ShaoYale University
Link to publication DOI Media Attached

Thu 19 Nov
Times are displayed in time zone: Central Time (US & Canada) change

05:00 - 06:20: W-6OOPSLA at SPLASH-I
Chair(s): John WickersonImperial College London, Jan VitekNortheastern University / Czech Technical University
05:00 - 05:20
Talk
Programming with a Read-Eval-Synth Loop
OOPSLA
Hila PelegUniversity of California at San Diego, Roi GabayTechnion, Shachar ItzhakyTechnion, Eran YahavTechnion
Link to publication DOI Media Attached
05:20 - 05:40
Talk
Sound Garbage Collection for C using Pointer Provenance
OOPSLA
Subarno BanerjeeUniversity of Michigan, David DevecseryGeorgia Institute of Technology, Peter M. ChenUniversity of Michigan, Satish NarayanasamyUniversity of Michigan
Link to publication DOI Media Attached
05:40 - 06:00
Talk
Semiring Optimizations: Dynamic Elision of Expressions with Identity and Absorbing Elements
OOPSLA
Guilherme Vieira LeobasFederal University of Minas Gerais, Fernando Magno Quintão PereiraFederal University of Minas Gerais
Link to publication DOI Pre-print Media Attached
06:00 - 06:20
Talk
CompCertELF: Verified Separate Compilation of C Programs into ELF Object Files
OOPSLA
Yuting WangShanghai Jiao Tong University, Xiangzhe XuNanjing University, Pierre WilkeCentraleSupélec, Zhong ShaoYale University
Link to publication DOI Media Attached