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

The Verified Software Toolchain is a tool for machine-checked proofs of correctness of C programs, with respect to specifications in separation logic and functional models in Coq. During the DeepSpec project (2015-2020) we have enhanced its program logic (Verifiable C) and its proof automation tools with better support for C control flow, concurrent shared-memory threads, more sophisticated separation-logic reasoning techniques, encapsulation of global variables, efficiency of separation-logic proof script execution, support for 64-bit or 32-bit C, many usability improvements, data abstraction, and strong support for modular proofs of modular programs. I will describe and illustrate some of these features.

Mon 15 Jun
Times are displayed in time zone: (GMT-07:00) Pacific Time (US & Canada) change

09:00 - 11:00: REMS-DeepSpec 2020 - REM-DeepSpec Session 3 at REMS/DeepSpec live stream
rems-deepspec-202009:00 - 09:40
Kayvan MemarianUniversity of Cambridge, Victor B. F. GomesUniversity of Cambridge, UK, Stella Lau, Jean Pichon-PharabodUniversity of Cambridge, UK, Justus MatthiesenUniversity of Cambridge, Peter SewellUniversity of Cambridge
rems-deepspec-202009:50 - 10:30
Andrew AppelPrinceton