Write a Blog >>
PLDI 2020
Mon 15 - Fri 19 June 2020
Wed 17 Jun 2020 10:40 - 11:00 at PLDI-Webinar - Verification I

Concurrent separation logics have had great success reasoning about
concurrent data structures.
This success stems from their application of modularity on multiple levels, leading to proofs that are decomposed according to program structure, program state, and individual threads.
Despite these advances, it remains difficult to achieve proof reuse across
different data structure implementations.
For the large class of \emph{search structures}, we demonstrate how one can achieve further proof modularity by decoupling the proof of thread safety from the proof of structural integrity.
We base our work on the \emph{template} algorithms of Shasha and
Goodman that dictate how threads interact but abstract from the
concrete layout of nodes in memory.
Building on the recently proposed flow framework of compositional abstractions and the separation logic Iris, we show how to prove correctness of template algorithms, and how to instantiate them to obtain multiple verified implementations.

We demonstrate our approach by mechanizing the proofs of three concurrent search
structure templates, based on link, give-up, and lock-coupling synchronization, and deriving verified implementations based on B-trees, hash tables, and linked lists.
These case studies include algorithms used in real-world file systems
and databases, which have been beyond the capability of prior automated or mechanized verification techniques.
In addition, our approach reduces proof complexity and is able to achieve significant proof reuse.

This program is tentative and subject to change.

Wed 17 Jun (GMT-07:00) Pacific Time (US & Canada) change

10:40 - 12:00: PLDI Research Papers - Verification I at PLDI-Webinar
pldi-2020-papers10:40 - 11:00
Siddharth KrishnaMicrosoft Research, USA, Nisarg PatelNew York University, USA, Dennis ShashaNew York University, USA, Thomas WiesNew York University, USA
pldi-2020-papers11:00 - 11:20
Jacob R. LorchMicrosoft Research, USA, Yixuan ChenUniversity of Michigan, USA / Yale University, USA, Manos KapritsosUniversity of Michigan, USA, Bryan ParnoCarnegie Mellon University, USA, Shaz QadeerCalibra, USA, Upamanyu SharmaUniversity of Michigan, USA, James R. WilcoxCertora, USA, Xueyuan ZhaoCarnegie Mellon University, USA
pldi-2020-papers11:20 - 11:40
Ori LahavTel Aviv University, Israel, Udi BokerIDC Herzliya, Israel
pldi-2020-papers11:40 - 12:00
Bernhard KraglIST Austria, Austria, Constantin EneaUniversity of Paris Diderot, France, Thomas A. HenzingerIST Austria, Austria, Suha Orhun MutluergilIRIF, France / University of Paris, France / CNRS, France, Shaz QadeerCalibra, USA