POPL 2024
Sun 14 - Sat 20 January 2024 London, United Kingdom
Wed 17 Jan 2024 14:00 - 14:20 at Turing Lecture - Automated Verification Chair(s): Gregory Malecha

Distributed protocols have long been formulated in terms of their safety and liveness properties. Much recent work has focused on automatically verifying the safety properties of distributed protocols, but doing so for liveness properties has remained a challenging, unsolved problem. We present LVR, the first framework that can automatically verify liveness properties for distributed protocols. Our key insight is that most liveness properties for distributed protocols can be reduced to a set of safety properties with the help of ranking functions. Such ranking functions for practical distributed protocols have certain properties that make them straightforward to synthesize, contrary to conventional wisdom. We prove that verifying a liveness property can then be reduced to a simpler problem of verifying a set of safety properties, namely that the ranking function is strictly decreasing and nonnegative for any protocol state transition, and there is no deadlock. LVR automatically synthesizes ranking functions by formulating a parameterized function of integer protocol variables, statically analyzing the lower and upper bounds of the variables as well as how much they can change on each state transition, then feeding the constraints to an SMT solver to determine the coefficients of the ranking function. It then uses an off-the-shelf verification tool to find inductive invariants to verify safety properties for both ranking functions and deadlock freedom. We show that LVR can mostly automatically verify the liveness properties of several distributed protocols, including various versions of Paxos.

Wed 17 Jan

Displayed time zone: London change

13:20 - 14:40
Automated VerificationPOPL at Turing Lecture
Chair(s): Gregory Malecha BedRock Systems
13:20
20m
Talk
Regular Abstractions for Array Systems
POPL
Chih-Duo Hong National Chengchi University, Anthony Widjaja Lin TU Kaiserslautern; MPI-SWS
13:40
20m
Talk
An Infinite Needle in a Finite Haystack: Finding Infinite Counter-Models in Deductive VerificationDistinguished Paper
POPL
Neta Elad Tel Aviv University, Oded Padon VMware Research, Sharon Shoham Tel Aviv University
Link to publication DOI
14:00
20m
Talk
Mostly Automated Verification of Liveness Properties for Distributed Protocols with Ranking FunctionsRemote
POPL
Jianan Yao Columbia University, Runzhou Tao Columbia University, Ronghui Gu Columbia University, Jason Nieh Columbia University
14:20
20m
Talk
Decision and Complexity of Dolev-Yao Hyperproperties
POPL
Itsaka Rakotonirina MPI-SP, Gilles Barthe MPI-SP; IMDEA Software Institute, Clara Schneidewind MPI-SP