Write a Blog >>
PLDI 2020
Mon 15 - Sat 20 June 2020
Wed 17 Jun 2020 11:00 - 11:20 at PLDI-Webinar - Verification I

Safely writing high-performance concurrent programs is notoriously difficult. To aid developers, we introduce Armada, a language and tool designed to formally verify such programs with relatively little effort. Via a C-like language and a small-step, state-machine-based semantics, Armada gives developers the flexibility to choose arbitrary memory layout and synchronization primitives so they are never constrained in their pursuit of performance. To reduce developer effort, Armada leverages SMT-powered automation and a library of powerful reasoning techniques, including rely-guarantee, TSO elimination, reduction, and alias analysis. All these techniques are proven sound, and Armada can be soundly extended with additional strategies over time. Using Armada, we verify four concurrent case studies and show that we can achieve performance equivalent to that of unverified code.

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