{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,11]],"date-time":"2026-03-11T01:47:33Z","timestamp":1773193653070,"version":"3.50.1"},"reference-count":45,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2024,1,2]],"date-time":"2024-01-02T00:00:00Z","timestamp":1704153600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000185","name":"DARPA","doi-asserted-by":"crossref","award":["66001-21-C-4018"],"award-info":[{"award-number":["66001-21-C-4018"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["CF-2124080, CCF-2239484, CNS-2052947, CNS-224737, NSF CAREER Award"],"award-info":[{"award-number":["CF-2124080, CCF-2239484, CNS-2052947, CNS-224737, NSF CAREER Award"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Amazon","award":["Amazon Research Award"],"award-info":[{"award-number":["Amazon Research Award"]}]},{"DOI":"10.13039\/100016682","name":"VMware","doi-asserted-by":"publisher","award":["VMWare Systems Research Award"],"award-info":[{"award-number":["VMWare Systems Research Award"]}],"id":[{"id":"10.13039\/100016682","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,1,2]]},"abstract":"<jats:p>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 mostly 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, with limited user guidance.<\/jats:p>","DOI":"10.1145\/3632877","type":"journal-article","created":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T20:48:51Z","timestamp":1704487731000},"page":"1028-1059","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":8,"title":["Mostly Automated Verification of Liveness Properties for Distributed Protocols with Ranking Functions"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0009-0008-4675-8980","authenticated-orcid":false,"given":"Jianan","family":"Yao","sequence":"first","affiliation":[{"name":"Columbia University, New York, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3733-5168","authenticated-orcid":false,"given":"Runzhou","family":"Tao","sequence":"additional","affiliation":[{"name":"Columbia University, New York, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6812-6182","authenticated-orcid":false,"given":"Ronghui","family":"Gu","sequence":"additional","affiliation":[{"name":"Columbia University, New York, USA"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-8301-4479","authenticated-orcid":false,"given":"Jason","family":"Nieh","sequence":"additional","affiliation":[{"name":"Columbia University, New York, USA"}]}],"member":"320","published-online":{"date-parts":[[2024,1,5]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","unstructured":"Mohamed Faouzi Atig Ahmed Bouajjani Michael Emmi and Akash Lal. 2012. Detecting fair non-termination in multithreaded programs. In Proceedings of 24th International Conference on Computer Aided Verification (CAV \u201912). 210\u2013226. https:\/\/doi.org\/10.1007\/978-3-642-31424-7_19 10.1007\/978-3-642-31424-7_19","DOI":"10.1007\/978-3-642-31424-7_19"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434325"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","unstructured":"Amir M Ben-Amram and Samir Genaim. 2017. On multiphase-linear ranking functions. In Proceedings ofthe 29th International Conference on Computer Aided Verification (CAV \u201917). 601\u2013620. https:\/\/doi.org\/10.1007\/978-3-319-63390-9_32 10.1007\/978-3-319-63390-9_32","DOI":"10.1007\/978-3-319-63390-9_32"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)80410-9"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","unstructured":"Benjamin Y. Chan and Elaine Shi. 2020. Streamlet: Textbook streamlined blockchains. In Proceedings of the 2nd ACM Conference on Advances in Financial Technologies (AFT \u201920). 1\u201311. https:\/\/doi.org\/10.1145\/3419614.3423256 10.1145\/3419614.3423256","DOI":"10.1145\/3419614.3423256"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","unstructured":"Michael A. Col\u00f3n and Henny B. Sipma. 2002. Practical methods for proving program termination. In Proceedings of 14th International Conference on Computer Aided Verification (CAV \u201902). 442\u2013454. https:\/\/doi.org\/10.1007\/3-540-45657-0_36 10.1007\/3-540-45657-0_36","DOI":"10.1007\/3-540-45657-0_36"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","unstructured":"Byron Cook Alexey Gotsman Andreas Podelski Andrey Rybalchenko and Moshe Y. Vardi. 2007a. Proving that programs eventually do something good. In Proceedings ofthe 34th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL \u201907). 265\u2013276. https:\/\/doi.org\/10.1145\/1190216.1190257 10.1145\/1190216.1190257","DOI":"10.1145\/1190216.1190257"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","unstructured":"Byron Cook Andreas Podelski and Andrey Rybalchenko. 2007b. Proving thread termination. In Proceedings ofthe 28th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI \u201907). 320\u2013330. https:\/\/doi.org\/10.1145\/1273442.1250771 10.1145\/1273442.1250771","DOI":"10.1145\/1273442.1250771"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","unstructured":"Byron Cook Abigail See and Florian Zuleger. 2013. Ramsey vs. lexicographic termination proving. In Proceedings ofthe 19th international conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS \u201913). 47\u201361. https:\/\/doi.org\/10.1007\/978-3-642-36742-7_4 10.1007\/978-3-642-36742-7_4","DOI":"10.1007\/978-3-642-36742-7_4"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","unstructured":"Azadeh Farzan Zachary Kincaid and Andreas Podelski. 2016. Proving liveness of parameterized programs. In Proceedings of the 31st Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS \u201916). 185\u2013196. https:\/\/doi.org\/10.1145\/2933575.2935310 10.1145\/2933575.2935310","DOI":"10.1145\/2933575.2935310"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","unstructured":"Marie Fortin Anca Muscholl and Igor Walukiewicz. 2017. Model-checking linear-time properties of parametrized asynchronous shared-memory pushdown systems. In Proceedings of 29th International Conference on Computer Aided Verification (CAV \u201917). 155\u2013175. https:\/\/doi.org\/10.1007\/978-3-319-63390-9_9 10.1007\/978-3-319-63390-9_9","DOI":"10.1007\/978-3-319-63390-9_9"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","unstructured":"Aman Goel and Karem Sakallah. 2021a. On symmetry and quantification: A new approach to verify distributed protocols. In Proceedings of the 13th NASA Formal Methods Symposium (NFM \u201921). 131\u2013150. https:\/\/doi.org\/10.1007\/978-3-030-76384-8_9 10.1007\/978-3-030-76384-8_9","DOI":"10.1007\/978-3-030-76384-8_9"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","unstructured":"Aman Goel and Karem A Sakallah. 2021b. Towards an automatic proof of Lamport\u2019s Paxos. In Proceedings of the 21st Conference on Formal Methods in Computer Aided Design (FMCAD \u201921). 112\u2013122. https:\/\/doi.org\/10.34727\/2021\/isbn.978-3-85448-046-4_20 10.34727\/2021\/isbn.978-3-85448-046-4_20","DOI":"10.34727\/2021\/isbn.978-3-85448-046-4_20"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","unstructured":"Laure Gonnord David Monniaux and Gabriel Radanne. 2015. Synthesis of ranking functions using extremal counterexamples. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI \u201915). 608\u2013618. https:\/\/doi.org\/10.1145\/2737924.2737976 10.1145\/2737924.2737976","DOI":"10.1145\/2737924.2737976"},{"key":"e_1_3_1_16_1","unstructured":"Travis Hance Marijn Heule Ruben Martins and Bryan Parno. 2021. Finding invariants of distributed systems: It\u2019s a small (enough) world after all. In Proceedings of the 18th USENIX Symposium on Networked Systems Design and Implementation (NSDI \u201921). 115\u2013131."},{"key":"e_1_3_1_17_1","unstructured":"Travis Hance Andrea Lattuada Chris Hawblitzel Jon Howell Rob Johnson and Bryan Parno. 2020. Storage systems are distributed systems (so verify them that way!). In Proceedings of the 14th USENIX Symposium on Operating Systems Design and Implementation (OSDI \u201920). 99\u2013115."},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","unstructured":"Chris Hawblitzel Jon Howell Manos Kapritsos Jacob R Lorch Bryan Parno Michael L Roberts Srinath Setty and Brian Zill. 2015a. IronFleet: Proving practical distributed systems correct. In Proceedings of the 25th Symposium on Operating Systems Principles (SOSP \u201915). 1\u201317. https:\/\/doi.org\/10.1145\/2815400.2815428 10.1145\/2815400.2815428","DOI":"10.1145\/2815400.2815428"},{"key":"e_1_3_1_19_1","doi-asserted-by":"crossref","unstructured":"Chris Hawblitzel Jon Howell Manos Kapritsos Jacob R Lorch Bryan Parno Michael L Roberts Srinath Setty and Brian Zill. 2015b. The IronFleet repository. https:\/\/github.com\/microsoft\/Ironclad\/tree\/main\/ironfleet.","DOI":"10.1145\/2815400.2815428"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-11(1:16)2015"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","unstructured":"Jochen Hoenicke Rupak Majumdar and Andreas Podelski. 2017. Thread modularity at many levels: A pearl in compositional verification. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL \u201917). 473\u2013485. https:\/\/doi.org\/10.1145\/3009837.3009893 10.1145\/3009837.3009893","DOI":"10.1145\/3009837.3009893"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3022187"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-3188-0"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","unstructured":"Jason R. Koenig Oded Padon Neil Immerman and Alex Aiken. 2020. First-order quantified separators. In Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI \u201920). 703\u2013717. https:\/\/doi.org\/10.1145\/3385412.3386018 10.1145\/3385412.3386018","DOI":"10.1145\/3385412.3386018"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","unstructured":"Jason R. Koenig Oded Padon Sharon Shoham and Alex Aiken. 2022. Inferring invariants with quantifier alternations: Taming the search space explosion. In Proceedings of the 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS \u201922). 338\u2013356. https:\/\/doi.org\/10.1007\/978-3-030-99524-9_18 10.1007\/978-3-030-99524-9_18","DOI":"10.1007\/978-3-030-99524-9_18"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","unstructured":"Bernhard Kragl Constantin Enea Thomas A Henzinger Suha Orhun Mutluergil and Shaz Qadeer. 2020. Inductive sequentialization of asynchronous programs. In Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI \u201920). 227\u2013242. https:\/\/doi.org\/10.1145\/3385412.3385980 10.1145\/3385412.3385980","DOI":"10.1145\/3385412.3385980"},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/279227.279229"},{"issue":"4","key":"e_1_3_1_28_1","first-page":"18","article-title":"Paxos made simple","volume":"32","author":"Lamport Leslie","year":"2001","unstructured":"Leslie Lamport. 2001. Paxos made simple. ACM Sigact News 32, 4 (2001), 18\u201325.","journal-title":"ACM Sigact News"},{"key":"e_1_3_1_29_1","unstructured":"Haojun Ma Hammad Ahmad Aman Goel Eli Goldweber Jean-Baptiste Jeannin Manos Kapritsos and Baris Kasikci. 2022. Sift: Using refinement-guided automation to verify complex distributed systems. In 2022 USENIX Annual Technical Conference (USENIX ATC \u201922). 151\u2013166."},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","unstructured":"Haojun Ma Aman Goel Jean-Baptiste Jeannin Manos Kapritsos Baris Kasikci and Karem A Sakallah. 2019. I4: Incremental inference of inductive invariants for verification of distributed protocols. In Proceedings of the 27th ACM Symposium on Operating Systems Principles (SOSP \u201919). 370\u2013384. https:\/\/doi.org\/10.1145\/3341301.3359651 10.1145\/3341301.3359651","DOI":"10.1145\/3341301.3359651"},{"key":"e_1_3_1_31_1","unstructured":"Dahlia Malkhi Leslie Lamport and Lidong Zhou. 2008. Stoppable Paxos. Technical Report MSR-TR-2008-192. https:\/\/www.microsoft.com\/en-us\/research\/publication\/stoppable-paxos\/"},{"key":"e_1_3_1_32_1","volume-title":"Proceedings of the 31st International Conference on Concurrency Theory (CONCUR \u201920)","author":"Neumann Eike","year":"2020","unstructured":"Eike Neumann, Jo\u00ebl Ouaknine, and James Worrell. 2020. On ranking function synthesis and termination for polynomial programs. In Proceedings of the 31st International Conference on Concurrency Theory (CONCUR \u201920). Schloss Dagstuhl-Leibniz-Zentrum f\u00fcr Informatik."},{"key":"e_1_3_1_33_1","unstructured":"Oded Padon. 2021. Source file of the ticket lock protocol in Ivy. https:\/\/github.com\/kenmcmil\/ivy\/blob\/master\/examples\/liveness\/ticket_nested.ivy."},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158114"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-021-00377-1"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","unstructured":"Oded Padon Kenneth L McMillan Aurojit Panda Mooly Sagiv and Sharon Shoham. 2016. Ivy: Safety verification by interactive generalization. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI \u201916). 614\u2013630. https:\/\/doi.org\/10.1145\/2908080.2908118 10.1145\/2908080.2908118","DOI":"10.1145\/2908080.2908118"},{"key":"e_1_3_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498712"},{"key":"e_1_3_1_38_1","doi-asserted-by":"publisher","unstructured":"Andreas Podelski and Andrey Rybalchenko. 2004. A complete method for the synthesis of linear ranking functions. In Proceedings of the 5th International Conference on Verification Model Checking and Abstract Interpretation (VMCAI \u201904). 239\u2013251. https:\/\/doi.org\/10.1007\/978-3-540-24622-0_20 10.1007\/978-3-540-24622-0_20","DOI":"10.1007\/978-3-540-24622-0_20"},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/58564.59295"},{"key":"e_1_3_1_40_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139168724"},{"key":"e_1_3_1_41_1","unstructured":"James Wilcox Oded Padon Yotam Feldman and other contributors. 2018. The mypyvy language. https:\/\/github.com\/wilcoxjay\/mypyvy."},{"key":"e_1_3_1_42_1","doi-asserted-by":"publisher","unstructured":"James R Wilcox Doug Woos Pavel Panchekha Zachary Tatlock Xi Wang Michael D Ernst and Thomas Anderson. 2015. Verdi: A framework for implementing and formally verifying distributed systems. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI \u201915). 357\u2013368. https:\/\/doi.org\/10.1145\/2737924.2737958 10.1145\/2737924.2737958","DOI":"10.1145\/2737924.2737958"},{"key":"e_1_3_1_43_1","doi-asserted-by":"publisher","unstructured":"Doug Woos James R Wilcox Steve Anton Zachary Tatlock Michael D Ernst and Thomas Anderson. 2016. Planning for change in a formal verification of the Raft consensus protocol. In Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs (CCP \u201916). 154\u2013165. https:\/\/doi.org\/10.1145\/2854065.2854081 10.1145\/2854065.2854081","DOI":"10.1145\/2854065.2854081"},{"key":"e_1_3_1_44_1","unstructured":"Jianan Yao Runzhou Tao Ronghui Gu and Jason Nieh. 2022. DuoAI: Fast automated inference of inductive invariants for verifying distributed protocols. In Proceedings of the 16th USENIX Symposium on Operating Systems Design and Implementation (OSDI \u201922). 485\u2013501."},{"key":"e_1_3_1_45_1","doi-asserted-by":"publisher","unstructured":"Jianan Yao Runzhou Tao Ronghui Gu and Jason Nieh. 2023. Mostly Automated Verification of Liveness Properties for Distributed Protocols with Ranking Functions (Artifact). https:\/\/doi.org\/10.5281\/zenodo.10039066 10.5281\/zenodo.10039066.","DOI":"10.5281\/zenodo.10039066"},{"key":"e_1_3_1_46_1","unstructured":"Jianan Yao Runzhou Tao Ronghui Gu Jason Nieh Suman Jana and Gabriel Ryan. 2021. DistAI: Data-driven automated invariant learning for distributed protocols. In Proceedings of the 15th USENIX Symposium on Operating Systems Design and Implementation (OSDI \u201921). 405\u2013421."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632877","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632877","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632877","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:07:24Z","timestamp":1751659644000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632877"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,2]]},"references-count":45,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2024,1,2]]}},"alternative-id":["10.1145\/3632877"],"URL":"https:\/\/doi.org\/10.1145\/3632877","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,1,2]]},"assertion":[{"value":"2024-01-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}