Mostly Automated Verification of Liveness Properties for Distributed Protocols with Ranking FunctionsRemote
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 JanDisplayed time zone: London change
13:20 - 14:40 | |||
13:20 20mTalk | Regular Abstractions for Array Systems POPL | ||
13:40 20mTalk | An Infinite Needle in a Finite Haystack: Finding Infinite Counter-Models in Deductive VerificationDistinguished Paper POPL Link to publication DOI | ||
14:00 20mTalk | 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 20mTalk | Decision and Complexity of Dolev-Yao Hyperproperties POPL Itsaka Rakotonirina MPI-SP, Gilles Barthe MPI-SP; IMDEA Software Institute, Clara Schneidewind MPI-SP |