{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,30]],"date-time":"2026-04-30T03:23:57Z","timestamp":1777519437903,"version":"3.51.4"},"reference-count":60,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2017,9,20]],"date-time":"2017-09-20T00:00:00Z","timestamp":1505865600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100002428","name":"Austrian Science Fund","doi-asserted-by":"publisher","award":["S11403"],"award-info":[{"award-number":["S11403"]}],"id":[{"id":"10.13039\/501100002428","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100002428","name":"Austrian Science Fund","doi-asserted-by":"publisher","award":["S11405"],"award-info":[{"award-number":["S11405"]}],"id":[{"id":"10.13039\/501100002428","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100002428","name":"Austrian Science Fund","doi-asserted-by":"publisher","award":["P27722"],"award-info":[{"award-number":["P27722"]}],"id":[{"id":"10.13039\/501100002428","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Austrian Science Fund (AT)","award":["W1255"],"award-info":[{"award-number":["W1255"]}]},{"DOI":"10.13039\/501100001821","name":"Vienna Science and Technology Fund","doi-asserted-by":"publisher","award":["ICT15-103"],"award-info":[{"award-number":["ICT15-103"]}],"id":[{"id":"10.13039\/501100001821","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2017,11]]},"DOI":"10.1007\/s10703-017-0297-4","type":"journal-article","created":{"date-parts":[[2017,9,20]],"date-time":"2017-09-20T15:03:52Z","timestamp":1505919832000},"page":"270-307","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["Para $$^2$$ 2 : parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms"],"prefix":"10.1007","volume":"51","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6629-3377","authenticated-orcid":false,"given":"Igor","family":"Konnov","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9222-6191","authenticated-orcid":false,"given":"Marijana","family":"Lazi\u0107","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Helmut","family":"Veith","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2795-611X","authenticated-orcid":false,"given":"Josef","family":"Widder","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,9,20]]},"reference":[{"key":"297_CR1","doi-asserted-by":"crossref","DOI":"10.1002\/0471478210","volume-title":"Distributed computing","author":"H Attiya","year":"2004","unstructured":"Attiya H, Welch J (2004) Distributed computing, 2nd edn. Wiley, New York","edition":"2"},{"key":"297_CR2","unstructured":"ByMC: Byzantine model checker (2013). http:\/\/forsyte.tuwien.ac.at\/software\/bymc\/ . Accessed Dec 2016"},{"issue":"5","key":"297_CR3","doi-asserted-by":"crossref","first-page":"401","DOI":"10.1007\/s10009-008-0064-3","volume":"10","author":"S Bardin","year":"2008","unstructured":"Bardin S, Finkel A, Leroux J, Petrucci L (2008) Fast: acceleration from theory to practice. STTT 10(5):401\u2013424","journal-title":"STTT"},{"key":"297_CR4","doi-asserted-by":"crossref","unstructured":"Basler G, Mazzucchi M, Wahl T, Kroening D (2009) Symbolic counter abstraction for concurrent software. In: CAV. LNCS, vol 5643, pp 64\u201378","DOI":"10.1007\/978-3-642-02658-4_9"},{"key":"297_CR5","unstructured":"Biere A (2013) Lingeling, Plingeling and Treengeling entering the SAT competition 2013. In: Proceedings of SAT competition 2013; Solver and p. 51"},{"key":"297_CR6","doi-asserted-by":"crossref","unstructured":"Biere A, Cimatti A, Clarke EM, Zhu Y (1999) Symbolic model checking without BDDs. In: TACAS. LNCS, vol 1579, pp 193\u2013207","DOI":"10.21236\/ADA360973"},{"key":"297_CR7","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-031-02011-7","volume-title":"Decidability of parameterized verification, synthesis lectures on distributed computing theory","author":"R Bloem","year":"2015","unstructured":"Bloem R, Jacobs S, Khalimov A, Konnov I, Rubin S, Veith H, Widder J (2015) Decidability of parameterized verification, synthesis lectures on distributed computing theory. Morgan & Claypool, San Rafael"},{"key":"297_CR8","doi-asserted-by":"crossref","unstructured":"Bokor P, Kinder J, Serafini M, Suri N (2011) Efficient model checking of fault-tolerant distributed protocols. In: DSN, pp 73\u201384","DOI":"10.1109\/DSN.2011.5958208"},{"issue":"4","key":"297_CR9","doi-asserted-by":"crossref","first-page":"824","DOI":"10.1145\/4221.214134","volume":"32","author":"G Bracha","year":"1985","unstructured":"Bracha G, Toueg S (1985) Asynchronous consensus and broadcast protocols. J ACM 32(4):824\u2013840","journal-title":"J ACM"},{"key":"297_CR10","doi-asserted-by":"crossref","unstructured":"Brasileiro FV, Greve F, Most\u00e9faoui A, Raynal M (2001) Consensus in one communication step. In: PaCT. LNCS, vol 2127, pp 42\u201350","DOI":"10.1007\/3-540-44743-1_4"},{"key":"297_CR11","doi-asserted-by":"crossref","unstructured":"Cavada R, Cimatti A, Dorigatti M, Griggio A, Mariotti A, Micheli A, Mover S, Roveri M, Tonetta S (2014) The nuXmv symbolic model checker. In: CAV. LNCS, vol 8559, pp 334\u2013342","DOI":"10.1007\/978-3-319-08867-9_22"},{"issue":"2","key":"297_CR12","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1145\/226643.226647","volume":"43","author":"TD Chandra","year":"1996","unstructured":"Chandra TD, Toueg S (1996) Unreliable failure detectors for reliable distributed systems. J ACM 43(2):225\u2013267","journal-title":"J ACM"},{"issue":"5","key":"297_CR13","doi-asserted-by":"crossref","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"E Clarke","year":"2003","unstructured":"Clarke E, Grumberg O, Jha S, Lu Y, Veith H (2003) Counterexample-guided abstraction refinement for symbolic model checking. J ACM 50(5):752\u2013794","journal-title":"J ACM"},{"key":"297_CR14","doi-asserted-by":"crossref","unstructured":"Clarke E, Talupur M, Touili T, Veith H (2004) Verification by network decomposition. In: CONCUR 2004, vol 3170, pp 276\u2013291","DOI":"10.1007\/978-3-540-28644-8_18"},{"key":"297_CR15","doi-asserted-by":"crossref","unstructured":"Clarke E, Talupur M, Veith H (2008) Proving Ptolemy right: the environment abstraction framework for model checking concurrent systems. In: TACAS\u201908\/ETAPS\u201908. Springer, Berlin, pp 33\u201347","DOI":"10.1007\/978-3-540-78800-3_4"},{"key":"297_CR16","doi-asserted-by":"crossref","unstructured":"Clarke EM, Kroening D, Ouaknine J, Strichman O (2004) Completeness and complexity of bounded model checking. In: VMCAI. LNCS, vol 2937, pp 85\u201396","DOI":"10.1007\/978-3-540-24622-0_9"},{"key":"297_CR17","unstructured":"De Moura L, Bj\u00f8rner N (2008) Z3: an efficient SMT solver. In: Tools and algorithms for the construction and analysis of systems. LNCS, vol 1579, pp 337\u2013340"},{"key":"297_CR18","doi-asserted-by":"crossref","unstructured":"Dobre D, Suri N (2006) One-step consensus with zero-degradation. In: DSN, pp 137\u2013146","DOI":"10.1109\/DSN.2006.55"},{"key":"297_CR19","doi-asserted-by":"crossref","unstructured":"Dr\u0103goi C, Henzinger TA, Zufferey D (2016) PSync: a partially synchronous language for fault-tolerant distributed algorithms. In: POPL, pp 400\u2013415","DOI":"10.1145\/2837614.2837650"},{"key":"297_CR20","doi-asserted-by":"crossref","unstructured":"Dr\u0103goi C, Henzinger TA, Veith H, Widder J, Zufferey D (2014) A logic-based framework for verifying consensus algorithms. In: VMCAI. LNCS, vol 8318, pp 161\u2013181","DOI":"10.1007\/978-3-642-54013-4_10"},{"key":"297_CR21","doi-asserted-by":"crossref","unstructured":"Emerson E, Namjoshi K (1995) Reasoning about rings. In: POPL, pp 85\u201394","DOI":"10.1145\/199448.199468"},{"key":"297_CR22","doi-asserted-by":"crossref","unstructured":"Emerson EA, Kahlon V (2003) Model checking guarded protocols. In: LICS. IEEE, pp 361\u2013370","DOI":"10.1109\/LICS.2003.1210076"},{"key":"297_CR23","doi-asserted-by":"crossref","unstructured":"Esparza J, Ganty P, Majumdar R (2013) Parameterized verification of asynchronous shared-memory systems. In: CAV, pp 124\u2013140","DOI":"10.1007\/978-3-642-39799-8_8"},{"key":"297_CR24","doi-asserted-by":"crossref","unstructured":"Farzan A, Kincaid Z, Podelski A (2013) Inductive data flow graphs. In: POPL, pp 129\u2013142","DOI":"10.1145\/2429069.2429086"},{"key":"297_CR25","doi-asserted-by":"crossref","unstructured":"Farzan A, Kincaid Z, Podelski A (2015) Proof spaces for unbounded parallelism. In: POPL, pp 407\u2013420","DOI":"10.1145\/2676726.2677012"},{"issue":"2","key":"297_CR26","doi-asserted-by":"crossref","first-page":"374","DOI":"10.1145\/3149.214121","volume":"32","author":"MJ Fischer","year":"1985","unstructured":"Fischer MJ, Lynch NA, Paterson MS (1985) Impossibility of distributed consensus with one faulty process. J ACM 32(2):374\u2013382","journal-title":"J ACM"},{"key":"297_CR27","doi-asserted-by":"crossref","unstructured":"Gmeiner A, Konnov I, Schmid U, Veith H, Widder J (2014) Tutorial on parameterized model checking of fault-tolerant distributed algorithms. In: SFM. LNCS, vol 8483. Springer, Berlin, pp 122\u2013171","DOI":"10.1007\/978-3-319-07317-0_4"},{"key":"297_CR28","unstructured":"Godefroid P (1990) Using partial orders to improve automatic verification methods. In: CAV. LNCS, vol 531, pp 176\u2013185"},{"issue":"1","key":"297_CR29","doi-asserted-by":"crossref","first-page":"17","DOI":"10.1007\/s446-002-8027-4","volume":"15","author":"R Guerraoui","year":"2002","unstructured":"Guerraoui R (2002) Non-blocking atomic commit in asynchronous distributed systems with failure detectors. Distrib Comput 15(1):17\u201325","journal-title":"Distrib Comput"},{"key":"297_CR30","unstructured":"https:\/\/github.com\/konnov\/fault-tolerant-benchmarks\/tree\/master\/fmsd17"},{"key":"297_CR31","doi-asserted-by":"crossref","unstructured":"Hawblitzel C, Howell J, Kapritsos M, Lorch JR, Parno B, Roberts ML, Setty STV, Zill B (2015) Ironfleet: proving practical distributed systems correct. In: SOSP, pp 1\u201317","DOI":"10.1145\/2815400.2815428"},{"key":"297_CR32","doi-asserted-by":"crossref","unstructured":"Jensen H, Lynch N (1998) A proof of Burns n-process mutual exclusion algorithm using abstraction. In: Steffen B (ed) TACAS. LNCS, vol 1384. Springer, Berlin, pp 409\u2013423","DOI":"10.1007\/BFb0054186"},{"key":"297_CR33","doi-asserted-by":"crossref","unstructured":"John A, Konnov I, Schmid U, Veith H, Widder J (2013) Parameterized model checking of fault-tolerant distributed algorithms by abstraction. In: FMCAD, pp 201\u2013209","DOI":"10.1109\/FMCAD.2013.6679411"},{"key":"297_CR34","doi-asserted-by":"crossref","unstructured":"John A, Konnov I, Schmid U, Veith H, Widder J (2013) Towards modeling and model checking fault-tolerant distributed algorithms. In: SPIN. LNCS, vol 7976, pp 209\u2013226","DOI":"10.1007\/978-3-642-39176-7_14"},{"key":"297_CR35","doi-asserted-by":"crossref","unstructured":"Kaiser A, Kroening D, Wahl T (2012) Efficient coverability analysis by proof minimization. In: CONCUR, pp 500\u2013515","DOI":"10.1007\/978-3-642-32940-1_35"},{"key":"297_CR36","doi-asserted-by":"crossref","first-page":"328","DOI":"10.1007\/s100090050040","volume":"2","author":"Y Kesten","year":"2000","unstructured":"Kesten Y, Pnueli A (2000) Control and data abstraction: the cornerstones of practical formal verification. STTT 2:328\u2013342","journal-title":"STTT"},{"key":"297_CR37","doi-asserted-by":"crossref","unstructured":"Konnov I, Lazi\u0107 M, Veith H, Widder J (2017) A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms. In: POPL, pp 719\u2013734","DOI":"10.1145\/3009837.3009860"},{"key":"297_CR38","doi-asserted-by":"crossref","unstructured":"Konnov I, Veith H, Widder J (2014) On the completeness of bounded model checking for threshold-based distributed algorithms: reachability. In: CONCUR. LNCS, vol 8704, pp 125\u2013140","DOI":"10.1007\/978-3-662-44584-6_10"},{"key":"297_CR39","doi-asserted-by":"crossref","unstructured":"Konnov I, Veith H, Widder J (2015) SMT and POR beat counter abstraction: parameterized model checking of threshold-based distributed algorithms. In: CAV (Part\u00a0I). LNCS, vol 9206, pp 85\u2013102","DOI":"10.1007\/978-3-319-21690-4_6"},{"key":"297_CR40","doi-asserted-by":"crossref","unstructured":"Konnov I, Veith H, Widder J (2016) What you always wanted to know about model checking of fault-tolerant distributed algorithms. In: PSI 2015, revised selected papers. LNCS, vol 9609. Springer, pp 6\u201321","DOI":"10.1007\/978-3-319-41579-6_2"},{"key":"297_CR41","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1016\/j.ic.2016.03.006","volume":"252","author":"I Konnov","year":"2017","unstructured":"Konnov I, Veith H, Widder J (2017) On the completeness of bounded model checking for threshold-based distributed algorithms: reachability. Inf Comput 252:95\u2013109","journal-title":"Inf Comput"},{"key":"297_CR42","doi-asserted-by":"crossref","unstructured":"Kroening D, Strichman O (2003) Efficient computation of recurrence diameters. In: VMCAI. LNCS, vol 2575, pp 298\u2013309","DOI":"10.1007\/3-540-36384-X_24"},{"issue":"7","key":"297_CR43","doi-asserted-by":"crossref","first-page":"558","DOI":"10.1145\/359545.359563","volume":"21","author":"L Lamport","year":"1978","unstructured":"Lamport L (1978) Time, clocks, and the ordering of events in a distributed system. Commun ACM 21(7):558\u2013565","journal-title":"Commun ACM"},{"key":"297_CR44","volume-title":"Specifying systems: the TLA+ language and tools for hardware and software engineers","author":"L Lamport","year":"2002","unstructured":"Lamport L (2002) Specifying systems: the TLA+ language and tools for hardware and software engineers. Addison-Wesley Longman Publishing Co. Inc, Boston"},{"key":"297_CR45","doi-asserted-by":"crossref","unstructured":"Leroux J, Sutre G (2004) On flatness for 2-dimensional vector addition systems with states. In: CONCUR 2004-concurrency theory. Springer, pp 402\u2013416","DOI":"10.1007\/978-3-540-28644-8_26"},{"key":"297_CR46","doi-asserted-by":"crossref","unstructured":"Leroux J, Sutre G (2005) Flat counter automata almost everywhere! In: ATVA. LNCS, vol 3707, pp 489\u2013503","DOI":"10.1007\/11562948_36"},{"key":"297_CR47","doi-asserted-by":"crossref","unstructured":"Lesani M, Bell CJ, Chlipala A (2016) Chapar: certified causally consistent distributed key-value stores. In: POPL, pp 357\u2013370","DOI":"10.1145\/2837614.2837622"},{"issue":"12","key":"297_CR48","doi-asserted-by":"crossref","first-page":"717","DOI":"10.1145\/361227.361234","volume":"18","author":"RJ Lipton","year":"1975","unstructured":"Lipton RJ (1975) Reduction: a method of proving properties of parallel programs. Commun ACM 18(12):717\u2013721","journal-title":"Commun ACM"},{"issue":"2","key":"297_CR49","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1007\/BF00289237","volume":"21","author":"BD Lubachevsky","year":"1984","unstructured":"Lubachevsky BD (1984) An approach to automating the verification of compact parallel coordination programs. I. Acta Inform 21(2):125\u2013169","journal-title":"Acta Inform"},{"key":"297_CR50","volume-title":"Distributed algorithms","author":"N Lynch","year":"1996","unstructured":"Lynch N (1996) Distributed algorithms. Morgan Kaufman, Burlington"},{"key":"297_CR51","doi-asserted-by":"crossref","unstructured":"Most\u00e9faoui A, Mourgaya E, Parv\u00e9dy PR, Raynal M (2003) Evaluating the condition-based approach to solve consensus. In: DSN, pp 541\u2013550","DOI":"10.1109\/DSN.2003.1209964"},{"key":"297_CR52","doi-asserted-by":"crossref","unstructured":"Padon O, McMillan KL, Panda A, Sagiv M, Shoham S (2016) Ivy: safety verification by interactive generalization. In: PLDI, pp 614\u2013630","DOI":"10.1145\/2908080.2908118"},{"key":"297_CR53","doi-asserted-by":"crossref","unstructured":"Peled D (1993) All from one, one for all: on model checking using representatives. In: CAV. LNCS, vol 697, pp 409\u2013423","DOI":"10.1007\/3-540-56922-7_34"},{"key":"297_CR54","doi-asserted-by":"crossref","unstructured":"Peluso S, Turcu A, Palmieri R, Losa G, Ravindran B (2016) Making fast consensus generally faster. In: DSN, pp 156\u2013167","DOI":"10.1109\/DSN.2016.23"},{"key":"297_CR55","unstructured":"Pnueli A, Xu J, Zuck L (2002) Liveness with (0,1,$\\infty $)-counter abstraction. In: CAV. LNCS, vol 2404, pp 93\u2013111"},{"key":"297_CR56","doi-asserted-by":"crossref","unstructured":"Raynal M (1997) A case study of agreement problems in distributed systems: non-blocking atomic commitment. In: HASE, pp 209\u2013214","DOI":"10.1109\/HASE.1997.648067"},{"key":"297_CR57","doi-asserted-by":"crossref","unstructured":"Song YJ, van Renesse R (2008) Bosco: one-step Byzantine asynchronous consensus. In: DISC. LNCS, vol 5218, pp 438\u2013450","DOI":"10.1007\/978-3-540-87779-0_30"},{"key":"297_CR58","doi-asserted-by":"crossref","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. Distrib Comput 2:80\u201394","journal-title":"Distrib Comput"},{"key":"297_CR59","doi-asserted-by":"crossref","unstructured":"Valmari A (1991) Stubborn sets for reduced state space generation. In: Advances in Petri Nets 1990. LNCS, vol 483. Springer, pp 491\u2013515","DOI":"10.1007\/3-540-53863-1_36"},{"key":"297_CR60","doi-asserted-by":"crossref","unstructured":"Wilcox JR, Woos D, Panchekha P, Tatlock Z, Wang X, Ernst MD, Anderson TE (2015) Verdi: a framework for implementing and formally verifying distributed systems. In: PLDI, pp 357\u2013368","DOI":"10.1145\/2737924.2737958"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-017-0297-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-017-0297-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-017-0297-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,3]],"date-time":"2022-08-03T03:12:46Z","timestamp":1659496366000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-017-0297-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,9,20]]},"references-count":60,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2017,11]]}},"alternative-id":["297"],"URL":"https:\/\/doi.org\/10.1007\/s10703-017-0297-4","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,9,20]]}}}