Keynote Talk: Pretend Synchrony: Synchronous Verification of Asynchronous Programs

Ranjit Jhala
UC San Diego (USA)

Ranjit Jhala is a professor of Computer Science and Engineering  at the University of California, San Diego. He works on algorithms  and tools that help engineer reliable computer systems. His work  draws from and contributes to the areas of Model Checking,  Program Analysis, and Automated Deduction, and Type Systems.  In particular, he is proud to have written some of the most cited papers in Programming Languages over the last fifteen years, and even more to have helped create several influential and award winning systems including the BLAST software model checker,  RELAY race detector, MACE/MC distributed language and model checker, and most recently, the LIQUIDHASKELL  refinement type checker.

We present pretend synchrony, a new approach to verifying distributed systems. Our approach is based on the observation that while distributed programs must execute asynchronously, we can often soundly treat them as if they were synchronous when verifying their correctness. To do so, we compute a synchronization, a semantically equivalent program where all sends, receives, and buffers, have been replaced by simple assignments, yielding a program that can be verified using Floyd-Hoare style Verification Conditions and SMT. We have implemented our approach and use four challenging case studies — the classic two phase commit protocol, a distributed key-value store, the Raft leader election protocol and single decree Paxos — to demonstrate that pretend synchrony makes verification of functional correctness simpler by reducing the manually specified invariants by a factor of 6, and faster by three orders of magnitude.


March 5th, 2021 @23:59 HST

Abstract submission deadline

March 12th, 2021 @23:59 HST

Paper submission deadline

April 26th, 2021

Acceptance notification

May 3rd, 2021 @23:59 HST

Camera ready copy due

May 10th, 2021 @23:59 HST

Pre-recorded talk

May 19th-21st, 2021

Online Conference with pre-recorded talks


Revised selected papers will be published as a post-proceedings in Springer's LNCS "Lecture Notes in Computer Science"

Partners & Sponsors