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
Times are displayed in time zone: (GMT-07:00) Pacific Time (US & Canada) change

09:00 - 11:00: REMS-DeepSpec 2020 - REMS-DeepSpec Session 6 at REMS/DeepSpec live stream
rems-deepspec-202009:00 - 09:40
Yannick ZakowskiUniversity of Pennsylvania
rems-deepspec-202009:50 - 10:30
Adam ChlipalaMassachusetts Institute of Technology, Andres Erbsen, Sam GruetterMassachusetts Institute of Technology, Joonwon ChoiMassachusetts Institute of Technology, USA