Write a Blog >>
PLDI 2020
Mon 15 - Fri 19 June 2020
Wed 17 Jun 2020 11:00 - 11:20 at PLDI Research Papers live stream - Verification I Chair(s): Stephen N. Freund

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.

Wed 17 Jun

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

10:40 - 12:00
10:40
20m
Talk
Verifying Concurrent Search Structure Templates
PLDI Research Papers
Siddharth Krishna Microsoft Research, Cambridge, Nisarg Patel New York University, USA, Dennis Shasha New York University, USA, Thomas Wies New York University, USA
11:00
20m
Talk
Armada: Low-Effort Verification of High-Performance Concurrent Programs
PLDI Research Papers
Jacob R. Lorch Microsoft Research, USA, Yixuan Chen University of Michigan, USA / Yale University, USA, Manos Kapritsos University of Michigan, USA, Bryan Parno Carnegie Mellon University, USA, Shaz Qadeer Novi, USA, Upamanyu Sharma University of Michigan, USA, James R. Wilcox Certora, USA, Xueyuan Zhao Carnegie Mellon University, USA
DOI
11:20
20m
Talk
Decidable Verification under a Causally Consistent Shared Memory
PLDI Research Papers
Ori Lahav Tel Aviv University, Israel, Udi Boker IDC Herzliya, Israel
11:40
20m
Talk
Inductive Sequentialization of Asynchronous Programs
PLDI Research Papers
Bernhard Kragl IST Austria, Constantin Enea University of Paris Diderot, France, Thomas A. Henzinger IST Austria, Austria, Suha Orhun Mutluergil IRIF, France / University of Paris, France / CNRS, France, Shaz Qadeer Novi, USA