Write a Blog >>
PLDI 2020
Mon 15 - Fri 19 June 2020
Tue 16 Jun 2020 09:50 - 10:30 at REMS/DeepSpec live stream - REMS-DeepSpec Session 6

We summarize the first DeepSpec project output that covers the whole scope envisioned for the larger effort, though with significantly simpler pieces, and only involving separate subteams within one of our institutions (though we promise that there was a genuine integration challenge here across artifacts that had been designed and implemented separately!). We introduced the project at last year’s DeepSpec workshop, and now the proofs are all connected and free of axioms beyond standard ones. The system is a controller for a lightbulb, accepting commands over an Ethernet card. We started by building the whole thing with conventional tools, beginning with a commercial RISC-V microcontroller, programmed with GCC-compiled C code. Then we replaced the hardware and software pieces separately with implementations inside Coq, showing that each could be dropped in to work properly with its mainstream counterpart. We designed a modular proof structure to help connect application code, device drivers, compiler, and processor without committing in advance to the profile of attached devices.

Tue 16 Jun

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

09:00 - 11:00
REMS-DeepSpec Session 6REMS-DeepSpec at REMS/DeepSpec live stream
Representing recursive and impure programs in Coq: from a toy assembly language to a modular formal semantics for LLVM IR
Yannick Zakowski University of Pennsylvania
The Verified IoT Lightbulb: Connecting Hardware and Software in a Simple Embedded System
Adam Chlipala Massachusetts Institute of Technology, Andres Erbsen , Samuel Gruetter Massachusetts Institute of Technology, Joonwon Choi Massachusetts Institute of Technology, USA