Tue 19 Jun 2018 16:35 - 16:40 at Columbus Ballroom B - Lightning Talks

The Vellvm project seeks to provide a formal framework for developing machine-checkable proofs about LLVM IR programs and translation passes. While the traditional SSA control-flow-graph representation used by this IR enforces rich invariants, reasoning about program equivalence of such CFGs can be difficult. In contrast, functional programming languages come with equational theories, allowing for program transformations to be proved without having to build manually a simulation.

In the Vellvm (Verified LLVM) project, we have been experimenting with representing SSA control-flow-graphs using terms of Levy’s call-by-push-value (CBPV) variant of the lambda calculus. CBPV offers the benefits of a good equational theory based on the usual notions of beta-equivalence. By relating the operational semantics of the CBPV language to that of the SSA-control-flow graphs, we can transport reasoning and program transformations from one level to another, thereby allowing for very simple proofs of the correctness of many low-level optimizations such as function inlining. This talk will give a high level overview of the ongoing work we are conducting to formalize this connection between SSA CFGs and CBPV.

This is joing work with: Dmitri Garbuzov, William Mansky, Christine Rizkallah, and Steve Zdancewic.

Tue 19 Jun
Times are displayed in time zone: (GMT-04:00) Eastern Time (US & Canada) change

16:10 - 17:35: DeepSpec 2018 - Lightning Talks at Columbus Ballroom B
deepspec-2018-papers16:10 - 16:15
deepspec-2018-papers16:15 - 16:20
deepspec-2018-papers16:20 - 16:25
Gordon StewartOhio University
deepspec-2018-papers16:25 - 16:30
deepspec-2018-papers16:30 - 16:35
deepspec-2018-papers16:35 - 16:40
deepspec-2018-papers16:40 - 16:45
Christine RizkallahUniversity of New South Wales
deepspec-2018-papers16:45 - 16:50
Joonwon ChoiMassachusetts Institute of Technology, USA
deepspec-2018-papers16:50 - 16:55
Sam GruetterMassachusetts Institute of Technology