SPLASH 2020
Sun 15 - Sat 21 November 2020 Online Conference
Fri 20 Nov 2020 13:00 - 13:20 at SPLASH-III - F-4B Chair(s): Aviral Goel, Ton Chanh Le
Sat 21 Nov 2020 01:00 - 01:20 at SPLASH-III - F-4B

CompCert is a moderately optimizing C compiler with a formal, machine-checked, proof of correctness: after successful compilation, the assembly code has a behavior faithful to the source code. Previously, it only supported target instruction sets with sequential semantics,
and did not attempt reordering instructions for optimization.

We present here a CompCert backend for a VLIW core (\textit{i.e.} with explicit parallelism at the instruction level), the first CompCert backend providing scalable and efficient instruction scheduling. Furthermore, its highly modular implementation can be easily adapted to other VLIW or non-VLIW pipelined processors.

Fri 20 Nov

Displayed time zone: Central Time (US & Canada) change

13:00 - 14:20
F-4BOOPSLA at SPLASH-III +12h
Chair(s): Aviral Goel Northeastern University, Ton Chanh Le Stevens Institute of Technology
13:00
20m
Talk
Certified and Efficient Instruction Scheduling: Application to Interlocked VLIW Processors
OOPSLA
Cyril Six Kalray / Grenoble Alps University / CNRS / Grenoble INP / VERIMAG, Sylvain Boulmé Grenoble Alps University / CNRS / Grenoble INP / VERIMAG, David Monniaux Grenoble Alps University / CNRS / Grenoble INP / VERIMAG
Link to publication DOI Media Attached
13:20
20m
Talk
Igloo: Soundly Linking Compositional Refinement and Separation Logic for Distributed System Verification
OOPSLA
Christoph Sprenger ETH Zurich, Tobias Klenze ETH Zurich, Marco Eilers ETH Zurich, Felix A. Wolf ETH Zurich, Peter Müller ETH Zurich, Martin Clochard ETH Zurich, David Basin ETH Zurich
Link to publication DOI Media Attached
13:40
20m
Talk
Neural Reverse Engineering of Stripped Binaries using Augmented Control Flow Graphs
OOPSLA
Yaniv David Technion, Uri Alon Technion, Eran Yahav Technion
Link to publication DOI Pre-print Media Attached
14:00
20m
Talk
Termination Analysis for Evolving Programs: An Incremental Approach by Reusing Certified Modules
OOPSLA
Fei He Tsinghua University, Jitao Han Tsinghua University
Link to publication DOI Media Attached

Sat 21 Nov

Displayed time zone: Central Time (US & Canada) change