{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:02:09Z","timestamp":1776304929795,"version":"3.50.1"},"reference-count":48,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2021,7,23]],"date-time":"2021-07-23T00:00:00Z","timestamp":1626998400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,7,23]],"date-time":"2021-07-23T00:00:00Z","timestamp":1626998400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"name":"Albert-Ludwigs-Universit\u00e4t Freiburg im Breisgau"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2021,8]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Various verification techniques for temporal properties transform temporal verification to safety verification. For infinite-state systems, these transformations are inherently imprecise. That is, for some instances, the temporal property holds, but the resulting safety property does not. This paper introduces a mechanism for tackling this imprecision. This mechanism, which we call <jats:italic>temporal prophecy<\/jats:italic>, is inspired by prophecy variables. Temporal prophecy refines an infinite-state system using first-order linear temporal logic formulas, via a suitable tableau construction. For a specific liveness-to-safety transformation based on first-order logic, we show that using temporal prophecy strictly increases the precision. Furthermore, temporal prophecy leads to robustness of the proof method, which is manifested by a cut elimination theorem. We integrate our approach into the Ivy deductive verification system, and show that it can handle challenging temporal verification examples.\n<\/jats:p>","DOI":"10.1007\/s10703-021-00377-1","type":"journal-article","created":{"date-parts":[[2021,7,23]],"date-time":"2021-07-23T08:03:02Z","timestamp":1627027382000},"page":"246-269","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Temporal prophecy for proving temporal properties of infinite-state systems"],"prefix":"10.1007","volume":"57","author":[{"given":"Oded","family":"Padon","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jochen","family":"Hoenicke","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kenneth L.","family":"McMillan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andreas","family":"Podelski","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mooly","family":"Sagiv","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sharon","family":"Shoham","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,7,23]]},"reference":[{"issue":"1","key":"377_CR1","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1016\/0304-3975(89)90138-2","volume":"65","author":"M Abadi","year":"1989","unstructured":"Abadi M (1989) The power of temporal proofs. Theor Comput Sci 65(1):35\u201383. https:\/\/doi.org\/10.1016\/0304-3975(89)90138-2","journal-title":"Theor Comput Sci"},{"issue":"2","key":"377_CR2","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1016\/0304-3975(91)90224-P","volume":"82","author":"M Abadi","year":"1991","unstructured":"Abadi M, Lamport L (1991) The existence of refinement mappings. Theor Comput Sci 82(2):253\u2013284. https:\/\/doi.org\/10.1016\/0304-3975(91)90224-P","journal-title":"Theor Comput Sci"},{"key":"377_CR3","doi-asserted-by":"crossref","unstructured":"Abdulla PA, Jonsson B, Rezine A, Saksena M (2006) Proving liveness by backwards reachability. In: CONCUR, lecture notes in computer science, vol 4137. Springer, pp 95\u2013109","DOI":"10.1007\/11817949_7"},{"key":"377_CR4","doi-asserted-by":"crossref","unstructured":"Babic D, Hu AJ, Rakamaric Z, Cook B (2007) Proving termination by divergence. In: SEFM, pp 93\u2013102","DOI":"10.1109\/SEFM.2007.32"},{"key":"377_CR5","doi-asserted-by":"crossref","unstructured":"Berkovits I, Lazic M, Lossa G, Padon O, Shoham S (2019) Verification of threshold-based distributed algorithms by decomposition to decidable logics. In: Computer aided verification\u201431th international conference, CAV","DOI":"10.1007\/978-3-030-25543-5_15"},{"issue":"2","key":"377_CR6","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1016\/S1571-0661(04)80410-9","volume":"66","author":"A Biere","year":"2002","unstructured":"Biere A, Artho C, Schuppan V (2002) Liveness checking as safety checking. Electr Notes Theor Comput Sci 66(2):160\u2013177","journal-title":"Electr Notes Theor Comput Sci"},{"key":"377_CR7","doi-asserted-by":"publisher","unstructured":"Black DL, Rashid RF, Golub DB, Hill CR (1989) Translation lookaside buffer consistency: a software approach. In: Proceedings of the third international conference on architectural support for programming languages and operating systems, ASPLOS III. ACM, New York, NY, USA, pp 113\u2013122. https:\/\/doi.org\/10.1145\/70082.68193","DOI":"10.1145\/70082.68193"},{"key":"377_CR8","doi-asserted-by":"crossref","unstructured":"Brockschmidt M, Cook B, Fuhs C (2013) Better termination proving through cooperation. In: Proceedings of the computer aided verification\u201425th international conference, CAV 2013, Saint Petersburg, Russia, July 13\u201319, 2013, pp 413\u2013429","DOI":"10.1007\/978-3-642-39799-8_28"},{"key":"377_CR9","doi-asserted-by":"publisher","unstructured":"Cook B, Khlaaf H, Piterman N (2015) On automation of ctl* verification for infinite-state systems. In: Kroening D, Pasareanu CS (eds) Proceedings of the computer aided verification\u201427th international conference, CAV 2015, San Francisco, CA, USA, July 18\u201324, 2015, Part I, lecture notes in computer science, vol 9206. Springer, pp 13\u201329. https:\/\/doi.org\/10.1007\/978-3-319-21690-4_2","DOI":"10.1007\/978-3-319-21690-4_2"},{"key":"377_CR10","doi-asserted-by":"publisher","unstructured":"Cook B, Koskinen E (2011) Making prophecies with decision predicates. In: Ball T, Sagiv M (eds) Proceedings of the 38th ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL 2011, Austin, TX, USA, January 26\u201328, 2011. ACM, pp 399\u2013410. https:\/\/doi.org\/10.1145\/1926385.1926431","DOI":"10.1145\/1926385.1926431"},{"key":"377_CR11","doi-asserted-by":"crossref","unstructured":"Cook B, Podelski A, Rybalchenko A (2006) Termination proofs for systems code. In: PLDI, pp 415\u2013426","DOI":"10.1145\/1133255.1134029"},{"issue":"5","key":"377_CR12","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1145\/1941487.1941509","volume":"54","author":"B Cook","year":"2011","unstructured":"Cook B, Podelski A, Rybalchenko A (2011) Proving program termination. Commun ACM 54(5):88\u201398","journal-title":"Commun ACM"},{"key":"377_CR13","doi-asserted-by":"crossref","unstructured":"Cook B, See A, Zuleger F (2013) Ramsey vs. lexicographic termination proving. In: TACAS, pp 47\u201361","DOI":"10.1007\/978-3-642-36742-7_4"},{"key":"377_CR14","unstructured":"Corbet J (2008) Ticket spinlocks. https:\/\/lwn.net\/Articles\/267968\/"},{"key":"377_CR15","doi-asserted-by":"crossref","unstructured":"Cousot P, Cousot R (2012) An abstract interpretation framework for termination. In: POPL, pp 245\u2013258","DOI":"10.1145\/2103621.2103687"},{"key":"377_CR16","doi-asserted-by":"crossref","unstructured":"Dietsch D, Heizmann M, Langenfeld V, Podelski A (2015) Fairness modulo theory: a new approach to LTL software model checking. In: CAV, lecture notes in computer science, vol 9206. Springer, pp 49\u201366","DOI":"10.1007\/978-3-319-21690-4_4"},{"key":"377_CR17","doi-asserted-by":"publisher","unstructured":"Fang Y, McMillan KL, Pnueli A, Zuck LD (2006) Liveness by invisible invariants. In: Najm E, Pradat-Peyre J, Donzeau-Gouge V (eds) Formal techniques for networked and distributed systems\u2014FORTE 2006, 26th IFIP WG 6.1 international conference, Paris, France, September 26\u201329, 2006. Lecture notes in computer science, vol 4229. Springer, pp 356\u2013371. https:\/\/doi.org\/10.1007\/11888116_26","DOI":"10.1007\/11888116_26"},{"key":"377_CR18","doi-asserted-by":"crossref","unstructured":"Farzan A, Kincaid Z, Podelski A (2016) Proving liveness of parameterized programs. In: LICS. ACM, pp 185\u2013196","DOI":"10.1145\/2933575.2935310"},{"key":"377_CR19","doi-asserted-by":"crossref","unstructured":"Ganty P, Genaim S (2013) Proving termination starting from the end. In: Proceedings of the computer aided verification\u201425th international conference, CAV 2013, Saint Petersburg, Russia, July 13\u201319, 2013, pp 397\u2013412","DOI":"10.1007\/978-3-642-39799-8_27"},{"key":"377_CR20","doi-asserted-by":"crossref","unstructured":"Ge Y, Moura LD (2009) Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In: International conference on computer aided verification. Springer, pp 306\u2013320","DOI":"10.1007\/978-3-642-02658-4_25"},{"key":"377_CR21","doi-asserted-by":"crossref","unstructured":"Giesl J, Thiemann R, Schneider-Kamp P, Falke S (2004) Automated termination proofs with AProVE. In: RTA, pp 210\u2013220","DOI":"10.1007\/978-3-540-25979-4_15"},{"key":"377_CR22","doi-asserted-by":"crossref","unstructured":"Grebenshchikov S, Lopes NP, Popeea C, Rybalchenko A (2012) Synthesizing software verifiers from proof rules. In: PLDI, pp 405\u2013416","DOI":"10.1145\/2345156.2254112"},{"key":"377_CR23","doi-asserted-by":"crossref","unstructured":"Gulwani S, Jain S, Koskinen E (2009) Control-flow refinement and progress invariants for bound analysis. In: PLDI, pp 375\u2013385","DOI":"10.1145\/1543135.1542518"},{"key":"377_CR24","doi-asserted-by":"crossref","unstructured":"Harris WR, Lal A, Nori AV, Rajamani SK (2010) Alternation for termination. In: Proceedings of the static analysis\u201417th international symposium, SAS 2010, Perpignan, France, September 14\u201316, 2010, pp 304\u2013319","DOI":"10.1007\/978-3-642-15769-1_19"},{"key":"377_CR25","doi-asserted-by":"crossref","unstructured":"Heizmann M, Hoenicke J, Podelski A (2014) Termination analysis by learning terminating programs. In: CAV, lecture notes in computer science, vol 8559. Springer, pp 797\u2013813","DOI":"10.1007\/978-3-319-08867-9_53"},{"key":"377_CR26","doi-asserted-by":"crossref","unstructured":"Hoenicke J, Majumdar R, Podelski A (2017) Thread modularity at many levels: a pearl in compositional verification. In: POPL. ACM, pp 473\u2013485","DOI":"10.1145\/3093333.3009893"},{"key":"377_CR27","doi-asserted-by":"crossref","unstructured":"Kesten Y, Pnueli A, Shahar E, Zuck LD (2002) Network invariants in action. In: Proceedings of the 13th international conference on concurrency theory, CONCUR \u201902. Springer, Berlin, pp 101\u2013115. http:\/\/dl.acm.org\/citation.cfm?id=646737.701938","DOI":"10.1007\/3-540-45694-5_8"},{"key":"377_CR28","doi-asserted-by":"crossref","unstructured":"Kroening D, Sharygina N, Tsitovich A, Wintersteiger CM (2010) Termination analysis with compositional transition invariants. In: Proceedings of the computer aided verification, 22nd international conference, CAV 2010, Edinburgh, UK, July 15\u201319, 2010, pp 89\u2013103","DOI":"10.1007\/978-3-642-14295-6_9"},{"key":"377_CR29","doi-asserted-by":"publisher","unstructured":"Lazic M, Konnov I, Widder J, Bloem R (2017) Synthesis of distributed algorithms with parameterized threshold guards. In: 21st international conference on principles of distributed systems, OPODIS 2017, Lisbon, Portugal, December 18\u201320, 2017, pp 32:1\u201332:20. https:\/\/doi.org\/10.4230\/LIPIcs.OPODIS.2017.32","DOI":"10.4230\/LIPIcs.OPODIS.2017.32"},{"key":"377_CR30","doi-asserted-by":"crossref","unstructured":"Lee W, Wang B, Yi K (2012) Termination analysis with algorithmic learning. In: 2012 Proceedings of the computer aided verification\u201424th international conference, CAV 2012, Berkeley, CA, USA, July 7\u201313, pp 88\u2013104","DOI":"10.1007\/978-3-642-31424-7_12"},{"key":"377_CR31","doi-asserted-by":"crossref","unstructured":"Manevich R, Dogadov B, Rinetzky N (2016) From shape analysis to termination analysis in linear time. In: CAV (1), lecture notes in computer science, vol 9779. Springer, pp 426\u2013446","DOI":"10.1007\/978-3-319-41528-4_23"},{"issue":"1\u20133","key":"377_CR32","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1016\/S0167-6423(99)00030-1","volume":"37","author":"KL McMillan","year":"2000","unstructured":"McMillan KL (2000) A methodology for hardware verification using compositional model checking. Sci Comput Program 37(1\u20133):279\u2013309. https:\/\/doi.org\/10.1016\/S0167-6423(99)00030-1","journal-title":"Sci Comput Program"},{"key":"377_CR33","doi-asserted-by":"crossref","unstructured":"McMillan KL, Padon O (2018) Deductive verification in decidable fragments with Ivy. In: SAS, lecture notes in computer science, vol 11002. Springer, pp 43\u201355","DOI":"10.1007\/978-3-319-99725-4_4"},{"key":"377_CR34","doi-asserted-by":"publisher","unstructured":"McMillan KL, Padon O (2020) Ivy: a multi-modal verification tool for distributed algorithms. In: Lahiri SK, Wang C (eds) Proceedings of the computer aided verification\u201432nd international conference, CAV 2020, Los Angeles, CA, USA, July 21\u201324, 2020, Part II, lecture notes in computer science, vol 12225. Springer, pp 190\u2013202. https:\/\/doi.org\/10.1007\/978-3-030-53291-8_12","DOI":"10.1007\/978-3-030-53291-8_12"},{"key":"377_CR35","doi-asserted-by":"crossref","unstructured":"Padon O (2019) Deductive verification of distributed protocols in first-order logic. Ph.D. thesis, Tel Aviv University","DOI":"10.23919\/FMCAD.2018.8603010"},{"issue":"POPL","key":"377_CR36","doi-asserted-by":"publisher","first-page":"26:1","DOI":"10.1145\/3158114","volume":"2","author":"O Padon","year":"2018","unstructured":"Padon O, Hoenicke J, Losa G, Podelski A, Sagiv M, Shoham S (2018) Reducing liveness to safety in first-order logic. PACMPL 2(POPL):26:1-26:33. https:\/\/doi.org\/10.1145\/3158114","journal-title":"PACMPL"},{"key":"377_CR37","doi-asserted-by":"crossref","unstructured":"Padon O, Hoenicke J, McMillan KL, Podelski A, Sagiv M, Shoham S (2018) Temporal prophecy for proving temporal properties of infinite-state systems. In: 2018 formal methods in computer-aided design, FMCAD 2018, Austin, Texas, USA, October 30\u2013November 2, 2018, pp 74\u201384","DOI":"10.23919\/FMCAD.2018.8603008"},{"key":"377_CR38","doi-asserted-by":"crossref","unstructured":"Padon O, McMillan KL, Panda A, Sagiv M, Shoham S (2016) Ivy: safety verification by interactive generalization. In: Proceedings of the 37th ACM SIGPLAN conference on programming language design and implementation, PLDI 2016, Santa Barbara, CA, USA, June 13\u201317, 2016, pp 614\u2013630","DOI":"10.1145\/2908080.2908118"},{"key":"377_CR39","doi-asserted-by":"crossref","unstructured":"Pnueli A, Shahar E (2000) Liveness and acceleration in parameterized verification. In: CAV, lecture notes in computer science, vol 1855. Springer, pp 328\u2013343","DOI":"10.1007\/10722167_26"},{"key":"377_CR40","doi-asserted-by":"crossref","unstructured":"Podelski A, Rybalchenko A (2004) Transition invariants. In: Proceedings of the 19th IEEE symposium on logic in computer science (LICS 2004), 14\u201317 July 2004, Turku, Finland, pp 32\u201341","DOI":"10.1109\/LICS.2004.1319598"},{"key":"377_CR41","doi-asserted-by":"crossref","unstructured":"Podelski A, Rybalchenko A (2005) Transition predicate abstraction and fair termination. In: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL 2005, Long Beach, California, USA, January 12\u201314, 2005, pp 132\u2013144","DOI":"10.1145\/1047659.1040317"},{"key":"377_CR42","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1007\/BF01667080","volume":"2","author":"T Srikanth","year":"1987","unstructured":"Srikanth T, Toueg S (1987) Simulating authenticated broadcasts to derive simple fault-tolerant algorithms. Dist Comput 2:80\u201394","journal-title":"Dist Comput"},{"key":"377_CR43","doi-asserted-by":"crossref","unstructured":"Urban C (2013) The abstract domain of segmented ranking functions. In: SAS, lecture notes in computer science, vol 7935. Springer, pp 43\u201362","DOI":"10.1007\/978-3-642-38856-9_5"},{"key":"377_CR44","doi-asserted-by":"crossref","unstructured":"Urban C, Gurfinkel A, Kahsai T (2016) Synthesizing ranking functions from bits and pieces. In: TACAS, lecture notes in computer science, vol 9636. Springer, pp 54\u201370","DOI":"10.1007\/978-3-662-49674-9_4"},{"key":"377_CR45","doi-asserted-by":"crossref","unstructured":"Urban C, Min\u00e9 A (2014) An abstract domain to infer ordinal-valued ranking functions. In: Proceedings of the programming languages and systems\u201423rd European symposium on programming, ESOP 2014, held as part of the European joint conferences on theory and practice of software, ETAPS 2014, Grenoble, France, April 5\u201313, 2014, pp 412\u2013431","DOI":"10.1007\/978-3-642-54833-8_22"},{"key":"377_CR46","doi-asserted-by":"crossref","unstructured":"Urban C, Min\u00e9 A (2014) A decision tree abstract domain for proving conditional termination. In: SAS, lecture notes in computer science, vol 8723. Springer, pp 302\u2013318","DOI":"10.1007\/978-3-319-10936-7_19"},{"key":"377_CR47","first-page":"77","volume":"47","author":"C Urban","year":"2017","unstructured":"Urban C, Min\u00e9 A (2017) Inference of ranking functions for proving temporal properties by abstract interpretation. Comput Lang Syst Struct 47:77\u2013103","journal-title":"Comput Lang Syst Struct"},{"issue":"2","key":"377_CR48","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/s00446-007-0026-0","volume":"20","author":"J Widder","year":"2007","unstructured":"Widder J, Schmid U (2007) Booting clock synchronization in partially synchronous systems with hybrid process and link failures. Dist Comput 20(2):115\u2013140","journal-title":"Dist Comput"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-021-00377-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-021-00377-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-021-00377-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,11,9]],"date-time":"2021-11-09T18:14:28Z","timestamp":1636481668000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-021-00377-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,7,23]]},"references-count":48,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2021,8]]}},"alternative-id":["377"],"URL":"https:\/\/doi.org\/10.1007\/s10703-021-00377-1","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,7,23]]},"assertion":[{"value":"30 April 2021","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"23 July 2021","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}