Mostly Automated Verification of Liveness Properties for Distributed Protocols with Ranking Functions

Explore a groundbreaking framework for mostly automated verification of liveness properties in distributed protocols in this 19-minute conference talk from POPL 2024. Delve into LVR, the first system of its kind that reduces liveness properties to safety properties using synthesized ranking functions. Learn how this approach simplifies the verification process for practical distributed protocols, challenging conventional wisdom. Discover the key insights behind LVR's methodology, including automatic synthesis of ranking functions and the use of off-the-shelf verification tools for safety property checks. Examine the framework's application to various versions of Paxos and other distributed protocols, demonstrating its effectiveness with limited user guidance. Gain access to supplementary materials, including reusable artifacts, to further understand and potentially implement this innovative approach in your own work on distributed systems verification.