{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:02:10Z","timestamp":1776304930210,"version":"3.50.1"},"reference-count":66,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2017,12,27]],"date-time":"2017-12-27T00:00:00Z","timestamp":1514332800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100011199","name":"FP7 Ideas: European Research Council","doi-asserted-by":"publisher","award":["321174"],"award-info":[{"award-number":["321174"]}],"id":[{"id":"10.13039\/100011199","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1655166"],"award-info":[{"award-number":["1655166"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100006221","name":"United States - Israel Binational Science Foundation","doi-asserted-by":"publisher","award":["2016260"],"award-info":[{"award-number":["2016260"]}],"id":[{"id":"10.13039\/100006221","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":[[2018,1]]},"abstract":"<jats:p>We develop a new technique for verifying temporal properties of infinite-state (distributed) systems. The main idea is to reduce the temporal verification problem to the problem of verifying the safety of infinite-state systems expressed in first-order logic. This allows to leverage existing techniques for safety verification to verify temporal properties of interesting distributed protocols, including some that have not been mechanically verified before. We model infinite-state systems using first-order logic, and use first-order temporal logic (FO-LTL) to specify temporal properties. This general formalism allows to naturally model distributed systems, while supporting both unbounded-parallelism (where the system is allowed to dynamically create processes), and infinite-state per process.<\/jats:p>\n          <jats:p>The traditional approach for verifying temporal properties of infinite-state systems employs well-founded relations (e.g. using linear arithmetic ranking functions). In contrast, our approach is based the idea of fair cycle detection. In finite-state systems, temporal verification can always be reduced to fair cycle detection (a system contains a fair cycle if it revisits a state after satisfying all fairness constraints). However, with both infinitely many states and infinitely many fairness constraints, a straightforward reduction to fair cycle detection is unsound. To regain soundness, we augment the infinite-state transition system by a dynamically computed finite set, that exploits the locality of transitions. This set lets us define a form of fair cycle detection that is sound in the presence of both infinitely many states, and infinitely many fairness constraints. Our approach allows a new style of temporal verification that does not explicitly involve ranking functions. This fits well with pure first-order verification which does not explicitly reason about numerical values. In particular, it can be used with effectively propositional first-order logic (EPR), in which case checking verification conditions is decidable. We applied our technique to verify temporal properties of several interesting protocols. To the best of our knowledge, we have obtained the first mechanized liveness proof for both TLB Shootdown, and Stoppable Paxos.<\/jats:p>","DOI":"10.1145\/3158114","type":"journal-article","created":{"date-parts":[[2017,12,29]],"date-time":"2017-12-29T14:21:49Z","timestamp":1514557309000},"page":"1-33","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":27,"title":["Reducing liveness to safety in first-order logic"],"prefix":"10.1145","volume":"2","author":[{"given":"Oded","family":"Padon","sequence":"first","affiliation":[{"name":"Tel Aviv University, Israel"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jochen","family":"Hoenicke","sequence":"additional","affiliation":[{"name":"University of Freiburg, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Giuliano","family":"Losa","sequence":"additional","affiliation":[{"name":"University of California at Los Angeles, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andreas","family":"Podelski","sequence":"additional","affiliation":[{"name":"University of Freiburg, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mooly","family":"Sagiv","sequence":"additional","affiliation":[{"name":"Tel Aviv University, Israel"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sharon","family":"Shoham","sequence":"additional","affiliation":[{"name":"Tel Aviv University, Israel"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2017,12,27]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(89)90138-2"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817949_7"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_11"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-12904-4_6"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2014.02.006"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36377-7_1"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)80410-9"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/70082.68193"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.2200\/S00658ED1V01Y201508DCT013"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190257"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1133981.1134029"},{"key":"e_1_2_2_12_1","unstructured":"Jonathan Corbet. 2008. Ticket spinlocks. https:\/\/lwn.net\/Articles\/267968\/ . (2008).  Jonathan Corbet. 2008. Ticket spinlocks. https:\/\/lwn.net\/Articles\/267968\/ . (2008)."},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103687"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41528-4_15"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_4"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/TIME.2008.15"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2914770.2837650"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/11888116_26"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2935310"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3149.214121"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1594834.1480886"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815428"},{"key":"e_1_2_2_24_1","volume-title":"Termination Analysis by Learning Terminating Programs. CoRR abs\/1405.4189","author":"Heizmann Matthias","year":"2014","unstructured":"Matthias Heizmann , Jochen Hoenicke , and Andreas Podelski . 2014. Termination Analysis by Learning Terminating Programs. CoRR abs\/1405.4189 ( 2014 ). Matthias Heizmann, Jochen Hoenicke, and Andreas Podelski. 2014. Termination Analysis by Learning Terminating Programs. CoRR abs\/1405.4189 (2014)."},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009893"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_40"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009860"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_6"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41579-6_2"},{"key":"e_1_2_2_30_1","volume-title":"4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 12-15, 2008, Proceedings. 292\u2013298","author":"Korovin Konstantin","year":"2008","unstructured":"Konstantin Korovin . 2008 . iProver - An Instantiation-Based Theorem Prover for First-Order Logic (System Description). In Automated Reasoning , 4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 12-15, 2008, Proceedings. 292\u2013298 . Konstantin Korovin. 2008. iProver - An Instantiation-Based Theorem Prover for First-Order Logic (System Description). In Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 12-15, 2008, Proceedings. 292\u2013298."},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_9"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_21"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/361082.361093"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/279227.279229"},{"key":"e_1_2_2_35_1","volume-title":"Paxos Made Simple. (December","author":"Lamport Leslie","year":"2001","unstructured":"Leslie Lamport . 2001. Paxos Made Simple. (December 2001 ), 51\u201358. https:\/\/www.microsoft.com\/en- us\/research\/publication\/ paxos- made- simple\/ Leslie Lamport. 2001. Paxos Made Simple. (December 2001), 51\u201358. https:\/\/www.microsoft.com\/en- us\/research\/publication\/ paxos- made- simple\/"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00446-006-0005-x"},{"key":"e_1_2_2_37_1","unstructured":"Leslie Lamport Dahlia Malkhi and Lidong Zhou. 2008. Stoppable Paxos. Technical Report. TechReport Microsoft Research. https:\/\/www.microsoft.com\/en- us\/research\/publication\/stoppable- paxos\/  Leslie Lamport Dahlia Malkhi and Lidong Zhou. 2008. Stoppable Paxos. Technical Report. TechReport Microsoft Research. https:\/\/www.microsoft.com\/en- us\/research\/publication\/stoppable- paxos\/"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1753171.1753191"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360210"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_12"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41528-4_23"},{"key":"e_1_2_2_42_1","volume-title":"Foundations of Computer Science: Distributed Systems","author":"Manna Zohar","unstructured":"Zohar Manna and Amir Pnueli . 1983. Verification of Concurrent Programs: A Temporal Proof System . In Foundations of Computer Science: Distributed Systems , J. W. de Bakker and J. van Leeuwen (Eds.). Mathematisch Centrum , Amsterdam , 163\u2013255. Zohar Manna and Amir Pnueli. 1983. Verification of Concurrent Programs: A Temporal Proof System. In Foundations of Computer Science: Distributed Systems, J. W. de Bakker and J. van Leeuwen (Eds.). Mathematisch Centrum, Amsterdam, 163\u2013255."},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-4222-2"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2016.7886668"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90182-F"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68679-8_22"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2012.06.003"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837667"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3140568"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908118"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9161-6"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31980-1_9"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45319-9_7"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_26"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24622-0_20"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2004.1319598"},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19835-9_2"},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1112\/plms\/s2-30.1.264"},{"key":"e_1_2_2_59_1","first-page":"3","article-title":"The Design and Implementation of VAMPIRE","volume":"15","author":"Riazanov Alexandre","year":"2002","unstructured":"Alexandre Riazanov and Andrei Voronkov . 2002 . The Design and Implementation of VAMPIRE . AI Commun. 15 , 2, 3 (Aug. 2002), 91\u2013110. http:\/\/dl.acm.org\/citation.cfm?id=1218615.1218620 Alexandre Riazanov and Andrei Voronkov. 2002. The Design and Implementation of VAMPIRE. AI Commun. 15, 2,3 (Aug. 2002), 91\u2013110. http:\/\/dl.acm.org\/citation.cfm?id=1218615.1218620","journal-title":"AI Commun."},{"key":"e_1_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/514188.514190"},{"key":"e_1_2_2_61_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.11.018"},{"key":"e_1_2_2_62_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.cl.2015.10.001"},{"key":"e_1_2_2_63_1","volume-title":"Proc. 1st Symp. on Logic in Computer Science","author":"Vardi M.Y.","unstructured":"M.Y. Vardi and P. Wolper . 1986. An Automata-Theoretic Approach to Automatic Program Verification . In Proc. 1st Symp. on Logic in Computer Science . Cambridge, 332\u2013344. http:\/\/www.cs.rice.edu\/~vardi\/papers\/lics86.pdf.gz M.Y. Vardi and P. Wolper. 1986. An Automata-Theoretic Approach to Automatic Program Verification. In Proc. 1st Symp. on Logic in Computer Science. Cambridge, 332\u2013344. http:\/\/www.cs.rice.edu\/~vardi\/papers\/lics86.pdf.gz"},{"key":"e_1_2_2_64_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02959-2_10"},{"key":"e_1_2_2_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737958"},{"key":"e_1_2_2_66_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44667-2_7"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3158114","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3158114","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3158114","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:11:30Z","timestamp":1750212690000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3158114"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,12,27]]},"references-count":66,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2018,1]]}},"alternative-id":["10.1145\/3158114"],"URL":"https:\/\/doi.org\/10.1145\/3158114","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,12,27]]},"assertion":[{"value":"2017-12-27","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}