{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,30]],"date-time":"2026-04-30T03:22:58Z","timestamp":1777519378046,"version":"3.51.4"},"publisher-location":"Cham","reference-count":60,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031711619","type":"print"},{"value":"9783031711626","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T00:00:00Z","timestamp":1726012800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T00:00:00Z","timestamp":1726012800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Threshold automata are a computational model that has proven to be versatile in modeling threshold-based distributed algorithms\u00a0and enabling their completely automatic parameterized verification. We present novel techniques for the verification of threshold automata, based on well-structured transition systems, that allow us to extend the expressiveness of both the computational model and the specifications that can be verified. In particular, we extend the model to allow decrements and resets of shared variables, possibly on cycles, and the specifications to general coverability. While these extensions of the model in general lead to undecidability, our algorithms provide a semi-decision procedure. We demonstrate the benefit of our extensions by showing that we can model complex round-based algorithms such as the phase king consensus algorithm and the Red Belly Blockchain protocol (published in 2019), and verify them fully automatically for the first time.<\/jats:p>","DOI":"10.1007\/978-3-031-71162-6_33","type":"book-chapter","created":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T02:02:27Z","timestamp":1725933747000},"page":"638-657","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Parameterized Verification of\u00a0Round-Based Distributed Algorithms via\u00a0Extended Threshold Automata"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0009-8539-6246","authenticated-orcid":false,"given":"Tom","family":"Baumeister","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-6117-318X","authenticated-orcid":false,"given":"Paul","family":"Eichler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9051-4050","authenticated-orcid":false,"given":"Swen","family":"Jacobs","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5160-0327","authenticated-orcid":false,"given":"Mouhammad","family":"Sakr","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8020-4446","authenticated-orcid":false,"given":"Marcus","family":"V\u00f6lp","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,9,11]]},"reference":[{"key":"33_CR1","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.K.: General decidability theorems for infinite-state systems. In: Proceedings 11th Annual IEEE Symposium on Logic in Computer Science, pp. 313\u2013321. IEEE (1996)","DOI":"10.1109\/LICS.1996.561359"},{"issue":"5","key":"33_CR2","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/S10009-015-0406-X","volume":"18","author":"PA Abdulla","year":"2016","unstructured":"Abdulla, P.A., Haziza, F., Hol\u00edk, L.: Parameterized verification through view abstraction. Int. J. Softw. Tools Technol. Transf. 18(5), 495\u2013516 (2016). https:\/\/doi.org\/10.1007\/S10009-015-0406-X","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"33_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/978-3-642-54013-4_15","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"B Aminof","year":"2014","unstructured":"Aminof, B., Jacobs, S., Khalimov, A., Rubin, S.: Parameterized model checking of token-passing systems. In: McMillan, K.L., Rival, X. (eds.) VMCAI 2014. LNCS, vol. 8318, pp. 262\u2013281. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54013-4_15"},{"key":"33_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/978-3-662-44584-6_9","volume-title":"CONCUR 2014 \u2013 Concurrency Theory","author":"B Aminof","year":"2014","unstructured":"Aminof, B., Kotek, T., Rubin, S., Spegni, F., Veith, H.: Parameterized model checking of rendezvous systems. In: Baldan, P., Gorla, D. (eds.) CONCUR 2014. LNCS, vol. 8704, pp. 109\u2013124. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-662-44584-6_9"},{"key":"33_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"476","DOI":"10.1007\/978-3-662-49122-5_23","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"S Au\u00dferlechner","year":"2016","unstructured":"Au\u00dferlechner, S., Jacobs, S., Khalimov, A.: Tight cutoffs for guarded protocols with fairness. In: Jobstmann, B., Leino, K.R.M. (eds.) VMCAI 2016. LNCS, vol. 9583, pp. 476\u2013494. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49122-5_23"},{"key":"33_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1007\/978-3-319-89963-3_3","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"AR Balasubramanian","year":"2018","unstructured":"Balasubramanian, A.R., Bertrand, N., Markey, N.: Parameterized verification of\u00a0synchronization in constrained reconfigurable broadcast networks. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10806, pp. 38\u201354. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89963-3_3"},{"key":"33_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/978-3-030-99253-8_4","volume-title":"Foundations of Software Science and Computation Structures","author":"AR Balasubramanian","year":"2022","unstructured":"Balasubramanian, A.R., Guillou, L., Weil-Kennedy, C.: Parameterized analysis of reconfigurable broadcast networks. In: FoSSaCS 2022. LNCS, vol. 13242, pp. 61\u201380. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99253-8_4"},{"key":"33_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1007\/978-3-030-59152-6_8","volume-title":"Automated Technology for Verification and Analysis","author":"AR Balasubramanian","year":"2020","unstructured":"Balasubramanian, A.R., Esparza, J., Lazi\u0107, M.: Complexity of verification and synthesis of threshold automata. In: Hung, D.V., Sokolsky, O. (eds.) ATVA 2020. LNCS, vol. 12302, pp. 144\u2013160. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-59152-6_8"},{"key":"33_CR9","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.12513748","author":"T Baumeister","year":"2024","unstructured":"Baumeister, T., Eichler, P., Jacobs, S., Sakr, M., V\u00f6lp, M.: Parameterized verification of round-based distributed algorithms via extended threshold automata -. Artifact (2024). https:\/\/doi.org\/10.5281\/zenodo.12513748","journal-title":"Artifact"},{"key":"33_CR10","unstructured":"Baumeister, T., Eichler, P., Jacobs, S., Sakr, M., V\u00f6lp, M.: Parameterized verification of round-based distributed algorithms via extended threshold automata (2024). https:\/\/arxiv.org\/abs\/2406.19880"},{"key":"33_CR11","doi-asserted-by":"crossref","unstructured":"Berman, P., Garay, J.A., Perry, K.J., et al.: Towards optimal distributed consensus. In: FOCS, vol. 89, pp. 410\u2013415 (1989)","DOI":"10.1109\/SFCS.1989.63511"},{"key":"33_CR12","doi-asserted-by":"crossref","unstructured":"Bertrand, N., Gramoli, V., Konnov, I., Lazic, M., Tholoniat, P., Widder, J.: Holistic verification of blockchain consensus. In: DISC. LIPIcs, vol.\u00a0246, pp. 10:1\u201310:24. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2022)","DOI":"10.1145\/3519270.3538468"},{"key":"33_CR13","doi-asserted-by":"publisher","unstructured":"Bertrand, N., Thomas, B., Widder, J.: Guard automata for the verification of safety and liveness of distributed algorithms. In: Haddad, S., Varacca, D. (eds.) 32nd International Conference on Concurrency Theory, CONCUR 2021, August 24\u201327, 2021, Virtual Conference. LIPIcs, vol.\u00a0203, pp. 15:1\u201315:17. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2021). https:\/\/doi.org\/10.4230\/LIPICS.CONCUR.2021.15","DOI":"10.4230\/LIPICS.CONCUR.2021.15"},{"key":"33_CR14","unstructured":"Bertrand, N., Thomas, B., Widder, J.: Guard automata for the verification of safety and liveness of distributed algorithms. In: Concur 2021-International Conference on Concurrency Theory, pp. 1\u201317 (2021)"},{"key":"33_CR15","doi-asserted-by":"publisher","unstructured":"Bloem, R., et al.: Decidability of Parameterized Verification. Synthesis Lectures on Distributed Computing Theory, Morgan & Claypool Publishers (2015). https:\/\/doi.org\/10.2200\/S00658ED1V01Y201508DCT013","DOI":"10.2200\/S00658ED1V01Y201508DCT013"},{"key":"33_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1007\/10722167_31","volume-title":"Computer Aided Verification","author":"A Bouajjani","year":"2000","unstructured":"Bouajjani, A., Jonsson, B., Nilsson, M., Touili, T.: Regular model checking. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 403\u2013418. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/10722167_31"},{"issue":"4","key":"33_CR17","doi-asserted-by":"publisher","first-page":"824","DOI":"10.1145\/4221.214134","volume":"32","author":"G Bracha","year":"1985","unstructured":"Bracha, G., Toueg, S.: Asynchronous consensus and broadcast protocols. J. ACM (JACM) 32(4), 824\u2013840 (1985)","journal-title":"J. ACM (JACM)"},{"key":"33_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1007\/3-540-44743-1_4","volume-title":"Parallel Computing Technologies","author":"F Brasileiro","year":"2001","unstructured":"Brasileiro, F., Greve, F., Mostefaoui, A., Raynal, M.: Consensus in one communication step. In: Malyshkin, V. (ed.) PaCT 2001. LNCS, vol. 2127, pp. 42\u201350. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44743-1_4"},{"key":"33_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1007\/3-540-44743-1_4","volume-title":"Parallel Computing Technologies","author":"F Brasileiro","year":"2001","unstructured":"Brasileiro, F., Greve, F., Mostefaoui, A., Raynal, M.: Consensus in one communication step. In: Malyshkin, V. (ed.) PaCT 2001. LNCS, vol. 2127, pp. 42\u201350. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44743-1_4"},{"issue":"2","key":"33_CR20","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1145\/226643.226647","volume":"43","author":"TD Chandra","year":"1996","unstructured":"Chandra, T.D., Toueg, S.: Unreliable failure detectors for reliable distributed systems. J. ACM (JACM) 43(2), 225\u2013267 (1996)","journal-title":"J. ACM (JACM)"},{"issue":"5","key":"33_CR21","doi-asserted-by":"publisher","first-page":"912","DOI":"10.1145\/355483.355489","volume":"47","author":"S Chaudhuri","year":"2000","unstructured":"Chaudhuri, S., Erlihy, M., Lynch, N.A., Tuttle, M.R.: Tight bounds for k-set agreement. J. ACM (JACM) 47(5), 912\u2013943 (2000)","journal-title":"J. ACM (JACM)"},{"key":"33_CR22","doi-asserted-by":"crossref","unstructured":"Crain, T., Gramoli, V., Larrea, M., Raynal, M.: DBFT: efficient leaderless byzantine consensus and its application to blockchains. In: 2018 IEEE 17th International Symposium on Network Computing and Applications (NCA), pp.\u00a01\u20138. IEEE (2018)","DOI":"10.1109\/NCA.2018.8548057"},{"key":"33_CR23","doi-asserted-by":"crossref","unstructured":"Crain, T., Natoli, C., Gramoli, V.: Red belly: a secure, fair and scalable open blockchain. In: SP, pp. 466\u2013483. IEEE (2021)","DOI":"10.1109\/SP40001.2021.00087"},{"key":"33_CR24","doi-asserted-by":"publisher","unstructured":"Czerwinski, W., Orlikowski, L.: Reachability in vector addition systems is Ackermann-complete. In: 62nd IEEE Annual Symposium on Foundations of Computer Science, FOCS 2021, Denver, CO, USA, February 7-10, 2022. pp. 1229\u20131240. IEEE (2021). https:\/\/doi.org\/10.1109\/FOCS52979.2021.00120","DOI":"10.1109\/FOCS52979.2021.00120"},{"key":"33_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"33_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1007\/978-3-642-15375-4_22","volume-title":"CONCUR 2010 - Concurrency Theory","author":"G Delzanno","year":"2010","unstructured":"Delzanno, G., Sangnier, A., Zavattaro, G.: Parameterized verification of ad hoc networks. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 313\u2013327. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15375-4_22"},{"key":"33_CR27","doi-asserted-by":"publisher","unstructured":"Emerson, E.A., Kahlon, V.: Model checking guarded protocols. In: LICS, pp. 361\u2013370. IEEE Computer Society (2003). https:\/\/doi.org\/10.1109\/LICS.2003.1210076","DOI":"10.1109\/LICS.2003.1210076"},{"issue":"4","key":"33_CR28","doi-asserted-by":"publisher","first-page":"527","DOI":"10.1142\/S0129054103001881","volume":"14","author":"EA Emerson","year":"2003","unstructured":"Emerson, E.A., Namjoshi, K.S.: On reasoning about rings. Found. Comput. Sci. 14(4), 527\u2013549 (2003). https:\/\/doi.org\/10.1142\/S0129054103001881","journal-title":"Found. Comput. Sci."},{"key":"33_CR29","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1007\/10721959_19","volume-title":"Automated Deduction - CADE-17","author":"EA Emerson","year":"2000","unstructured":"Emerson, E.A., Kahlon, V.: Reducing model checking of the many to the few. In: McAllester, D. (ed.) CADE 2000. LNCS (LNAI), vol. 1831, pp. 236\u2013254. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/10721959_19"},{"key":"33_CR30","doi-asserted-by":"publisher","unstructured":"Esparza, J., Finkel, A., Mayr, R.: On the verification of broadcast protocols. In: LICS, pp. 352\u2013359. IEEE Computer Society (1999). https:\/\/doi.org\/10.1109\/LICS.1999.782630","DOI":"10.1109\/LICS.1999.782630"},{"key":"33_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"210","DOI":"10.1007\/3-540-56689-9_45","volume-title":"Advances in Petri Nets 1993","author":"A Finkel","year":"1993","unstructured":"Finkel, A.: The minimal coverability graph for Petri nets. In: Rozenberg, G. (ed.) ICATPN 1991. LNCS, vol. 674, pp. 210\u2013243. Springer, Heidelberg (1993). https:\/\/doi.org\/10.1007\/3-540-56689-9_45"},{"issue":"1\u20132","key":"33_CR32","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1016\/S0304-3975(00)00102-X","volume":"256","author":"A Finkel","year":"2001","unstructured":"Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere! Theoret. Comput. Sci. 256(1\u20132), 63\u201392 (2001)","journal-title":"Theoret. Comput. Sci."},{"issue":"3","key":"33_CR33","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1145\/146637.146681","volume":"39","author":"SM German","year":"1992","unstructured":"German, S.M., Sistla, A.P.: Reasoning about systems with many processes. J. ACM 39(3), 675\u2013735 (1992). https:\/\/doi.org\/10.1145\/146637.146681","journal-title":"J. ACM"},{"issue":"1","key":"33_CR34","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/s446-002-8027-4","volume":"15","author":"R Guerraoui","year":"2002","unstructured":"Guerraoui, R.: Non-blocking atomic commit in asynchronous distributed systems with failure detectors. Distrib. Comput. 15(1), 17\u201325 (2002)","journal-title":"Distrib. Comput."},{"key":"33_CR35","doi-asserted-by":"publisher","unstructured":"Hawblitzel, C., et al.: Ironfleet: proving safety and liveness of practical distributed systems. Commun. ACM 60(7), 83\u201392 (2017). https:\/\/doi.org\/10.1145\/3068608","DOI":"10.1145\/3068608"},{"key":"33_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/978-3-030-53288-8_15","volume-title":"Computer Aided Verification","author":"N Jaber","year":"2020","unstructured":"Jaber, N., Jacobs, S., Wagner, C., Kulkarni, M., Samanta, R.: Parameterized verification of systems with global synchronization and guards. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12224, pp. 299\u2013323. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53288-8_15"},{"key":"33_CR37","doi-asserted-by":"publisher","unstructured":"Jaber, N., Wagner, C., Jacobs, S., Kulkarni, M., Samanta, R.: Quicksilver: modeling and parameterized verification for distributed agreement-based systems. Proc. ACM Program. Lang. 5(OOPSLA), 1\u201331 (2021). https:\/\/doi.org\/10.1145\/3485534","DOI":"10.1145\/3485534"},{"key":"33_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/978-3-319-73721-8_12","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"S Jacobs","year":"2018","unstructured":"Jacobs, S., Sakr, M.: Analyzing guarded protocols: better cutoffs, more systems, more expressivity. In: VMCAI 2018. LNCS, vol. 10747, pp. 247\u2013268. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-73721-8_12"},{"key":"33_CR39","unstructured":"Jacobs, S., Sakr, M., V\u00f6lp, M.: Automatic repair and deadlock detection for parameterized systems. In: Conference on Formal Methods in Computer-Aided Design\u2013FMCAD 2022, p.\u00a0225 (2022)"},{"key":"33_CR40","doi-asserted-by":"crossref","unstructured":"John, A., Konnov, I., Schmid, U., Veith, H., Widder, J.: Parameterized model checking of fault-tolerant distributed algorithms by abstraction. In: 2013 Formal Methods in Computer-Aided Design. pp. 201\u2013209. IEEE (2013)","DOI":"10.1109\/FMCAD.2013.6679411"},{"key":"33_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"645","DOI":"10.1007\/978-3-642-14295-6_55","volume-title":"Computer Aided Verification","author":"A Kaiser","year":"2010","unstructured":"Kaiser, A., Kroening, D., Wahl, T.: Dynamic cutoff detection in parameterized concurrent programs. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 645\u2013659. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_55"},{"key":"33_CR42","unstructured":"Konnov, I.: Fault-tolerant benchmarks. https:\/\/github.com\/konnov\/fault-tolerant-benchmarks\/tree\/master\/cav15"},{"issue":"2","key":"33_CR43","doi-asserted-by":"publisher","first-page":"270","DOI":"10.1007\/s10703-017-0297-4","volume":"51","author":"I Konnov","year":"2017","unstructured":"Konnov, I., Lazi\u0107, M., Veith, H., Widder, J.: Para 2: parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms. Formal Meth. Syst. Des. 51(2), 270\u2013307 (2017)","journal-title":"Formal Meth. Syst. Des."},{"key":"33_CR44","doi-asserted-by":"crossref","unstructured":"Konnov, I., Lazi\u0107, M., Veith, H., Widder, J.: A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms. In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, pp. 719\u2013734 (2017)","DOI":"10.1145\/3009837.3009860"},{"key":"33_CR45","doi-asserted-by":"publisher","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.: On the completeness of bounded model checking for threshold-based distributed algorithms: reachability. Inf. Comput. 252, 95\u2013109 (2017)","journal-title":"Inf. Comput."},{"key":"33_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1007\/978-3-030-03424-5_22","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Distributed Systems","author":"I Konnov","year":"2018","unstructured":"Konnov, I., Widder, J.: ByMC: byzantine model checker. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018. LNCS, vol. 11246, pp. 327\u2013342. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-03424-5_22"},{"key":"33_CR47","unstructured":"Kukovec, J., Konnov, I., Widder, J.: Reachability in parameterized systems: all flavors of threshold automata. In: CONCUR 2018-29th International Conference on Concurrency Theory (2018)"},{"key":"33_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/978-3-319-63390-9_12","volume-title":"Computer Aided Verification","author":"O Mari\u0107","year":"2017","unstructured":"Mari\u0107, O., Sprenger, C., Basin, D.: Cutoff bounds for consensus algorithms. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 217\u2013237. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63390-9_12"},{"key":"33_CR49","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1007\/978-3-030-53291-8_12","volume-title":"Computer Aided Verification","author":"KL McMillan","year":"2020","unstructured":"McMillan, K.L., Padon, O.: Ivy: a multi-modal verification tool for distributed algorithms. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12225, pp. 190\u2013202. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53291-8_12"},{"key":"33_CR50","doi-asserted-by":"crossref","unstructured":"Most\u00e9faoui, A., Mourgaya, E., Parv\u00e9dy, P.R., Raynal, M.: Evaluating the condition-based approach to solve consensus. In: 2003 International Conference on Dependable Systems and Networks, 2003. Proceedings, pp. 541\u2013541. IEEE Computer Society (2003)","DOI":"10.1109\/DSN.2003.1209964"},{"issue":"2","key":"33_CR51","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1016\/0304-3975(78)90036-1","volume":"6","author":"C Rackoff","year":"1978","unstructured":"Rackoff, C.: The covering and boundedness problems for vector addition systems. Theoret. Comput. Sci. 6(2), 223\u2013231 (1978)","journal-title":"Theoret. Comput. Sci."},{"key":"33_CR52","doi-asserted-by":"publisher","unstructured":"Rahli, V., Guaspari, D., Bickford, M., Constable, R.L.: Formal specification, verification, and implementation of fault-tolerant systems using eventml. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 72 (2015). https:\/\/doi.org\/10.14279\/TUJ.ECEASST.72.1013","DOI":"10.14279\/TUJ.ECEASST.72.1013"},{"key":"33_CR53","doi-asserted-by":"crossref","unstructured":"Raynal, M.: A case study of agreement problems in distributed systems: non-blocking atomic commitment. In: Proceedings 1997 High-Assurance Engineering Workshop, pp. 209\u2013214. IEEE (1997)","DOI":"10.1109\/HASE.1997.648067"},{"key":"33_CR54","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/978-3-642-40184-8_2","volume-title":"CONCUR 2013 \u2013 Concurrency Theory","author":"S Schmitz","year":"2013","unstructured":"Schmitz, S., Schnoebelen, P.: The power of well-structured systems. In: D\u2019Argenio, P.R., Melgratti, H. (eds.) CONCUR 2013. LNCS, vol. 8052, pp. 5\u201324. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40184-8_2"},{"key":"33_CR55","unstructured":"Somenzi, F.: CUDD: cu decision diagram package release 2.3. 0. University of Colorado at Boulder 621 (1998)"},{"key":"33_CR56","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"438","DOI":"10.1007\/978-3-540-87779-0_30","volume-title":"Distributed Computing","author":"YJ Song","year":"2008","unstructured":"Song, Y.J., van Renesse, R.: Bosco: one-step byzantine asynchronous consensus. In: Taubenfeld, G. (ed.) DISC 2008. LNCS, vol. 5218, pp. 438\u2013450. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-87779-0_30"},{"issue":"2","key":"33_CR57","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1007\/BF01667080","volume":"2","author":"T Srikanth","year":"1987","unstructured":"Srikanth, T., Toueg, S.: Simulating authenticated broadcasts to derive simple fault-tolerant algorithms. Distrib. Comput. 2(2), 80\u201394 (1987)","journal-title":"Distrib. Comput."},{"issue":"4","key":"33_CR58","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1016\/0020-0190(88)90211-6","volume":"28","author":"I Suzuki","year":"1988","unstructured":"Suzuki, I.: Proving properties of a ring of finite-state machines. Inf. Process. Lett. 28(4), 213\u2013214 (1988). https:\/\/doi.org\/10.1016\/0020-0190(88)90211-6","journal-title":"Inf. Process. Lett."},{"key":"33_CR59","doi-asserted-by":"publisher","unstructured":"Thomas, B., Sankur, O.: Pylta: a verification tool for parameterized distributed algorithms. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 28\u201335. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-30820-8_4","DOI":"10.1007\/978-3-031-30820-8_4"},{"key":"33_CR60","doi-asserted-by":"publisher","unstructured":"Wilcox, J.R., et al.: Verdi: a framework for implementing and formally verifying distributed systems. In: Grove, D., Blackburn, S.M. (eds.) Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, Portland, OR, USA, June 15\u201317, 2015, pp. 357\u2013368. ACM (2015). https:\/\/doi.org\/10.1145\/2737924.2737958","DOI":"10.1145\/2737924.2737958"}],"container-title":["Lecture Notes in Computer Science","Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-71162-6_33","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,27]],"date-time":"2024-11-27T23:01:59Z","timestamp":1732748519000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-71162-6_33"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,9,11]]},"ISBN":["9783031711619","9783031711626"],"references-count":60,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-71162-6_33","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,9,11]]},"assertion":[{"value":"11 September 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The program, benchmark scripts and the benchmark files as evaluated in Sect.\u00a0are available at.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Data Availability"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Milan","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 September 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 September 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.fm24.polimi.it\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}