{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T12:11:40Z","timestamp":1781007100469,"version":"3.54.1"},"reference-count":50,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2021,8,30]],"date-time":"2021-08-30T00:00:00Z","timestamp":1630281600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,8,30]],"date-time":"2021-08-30T00:00:00Z","timestamp":1630281600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2022,2]]},"DOI":"10.1007\/s10009-021-00637-9","type":"journal-article","created":{"date-parts":[[2021,8,30]],"date-time":"2021-08-30T05:15:34Z","timestamp":1630300534000},"page":"33-48","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Verifying safety of synchronous fault-tolerant algorithms by bounded model checking"],"prefix":"10.1007","volume":"24","author":[{"given":"Ilina","family":"Stoilkovska","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Igor","family":"Konnov","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Josef","family":"Widder","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Florian","family":"Zuleger","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2021,8,30]]},"reference":[{"key":"637_CR1","doi-asserted-by":"crossref","unstructured":"Stoilkovska, I., Konnov, I., Widder, J., Zuleger, F.: Verifying safety of synchronous fault-tolerant algorithms by bounded model checking. In: T.\u00a0Vojnar, L.\u00a0Zhang (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part II, Lecture Notes in Computer Science, vol. 11428, pp. 357\u2013374. Springer (2019)","DOI":"10.1007\/978-3-030-17465-1_20"},{"issue":"7","key":"637_CR2","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1145\/3068608","volume":"60","author":"C Hawblitzel","year":"2017","unstructured":"Hawblitzel, C., Howell, J., Kapritsos, M., Lorch, J.R., Parno, B., Roberts, M.L., Setty, S.T.V., Zill, B.: Ironfleet: proving safety and liveness of practical distributed systems. Commun. ACM 60(7), 83\u201392 (2017)","journal-title":"Commun. ACM"},{"key":"637_CR3","doi-asserted-by":"crossref","unstructured":"Wilcox, J.R., Woos, D., Panchekha, P., Tatlock, Z., Wang, X., Ernst, M.D., Anderson, T.E.: Verdi: a framework for implementing and formally verifying distributed systems. In: PLDI, pp. 357\u2013368 (2015)","DOI":"10.1145\/2813885.2737958"},{"key":"637_CR4","doi-asserted-by":"crossref","unstructured":"Sergey, I., Wilcox, J.R., Tatlock, Z.: Programming and proving with distributed protocols. In: PACMPL 2(POPL), pp. 28:1\u201328:30 (2018)","DOI":"10.1145\/3158116"},{"key":"637_CR5","doi-asserted-by":"crossref","unstructured":"Desai, A., Garg, P., Madhusudan, P.: Natural proofs for asynchronous programs using almost-synchronous reductions. In: Proceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages & Applications, OOPSLA 2014, part of SPLASH 2014, Portland, OR, USA, October 20-24, 2014, pp. 709\u2013725 (2014)","DOI":"10.1145\/2660193.2660211"},{"key":"637_CR6","doi-asserted-by":"crossref","unstructured":"Berkovits, I., Lazic, M., Losa, G., Padon, O., Shoham, S.: Verification of threshold-based distributed algorithms by decomposition to decidable logics. In: I.\u00a0Dillig, S.\u00a0Tasiran (eds.) Computer Aided Verification - 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part II, Lecture Notes in Computer Science, vol. 11562, pp. 245\u2013266. Springer (2019)","DOI":"10.1007\/978-3-030-25543-5_15"},{"key":"637_CR7","doi-asserted-by":"crossref","unstructured":"Padon, O., McMillan, K.L., Panda, A., Sagiv, M., Shoham, S.: Ivy: safety verification by interactive generalization. In: PLDI, pp. 614\u2013630 (2016)","DOI":"10.1145\/2980983.2908118"},{"key":"637_CR8","doi-asserted-by":"crossref","unstructured":"Dr\u0103goi, C., Henzinger, T.A., Veith, H., Widder, J., Zufferey, D.: A Logic-Based Framework for Verifying Consensus Algorithms. In: VMCAI, LNCS 8318, 161\u2013181 (2014)","DOI":"10.1007\/978-3-642-54013-4_10"},{"key":"637_CR9","doi-asserted-by":"crossref","unstructured":"Dr\u0103goi, C., Henzinger, T.A., Zufferey, D.: Psync: a partially synchronous language for fault-tolerant distributed algorithms. In: POPL, pp. 400\u2013415 (2016)","DOI":"10.1145\/2914770.2837650"},{"key":"637_CR10","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Enea, C., Ji, K., Qadeer, S.: On the completeness of verifying message passing programs under bounded asynchrony. In: CAV, pp. 372\u2013391 (2018)","DOI":"10.1007\/978-3-319-96142-2_23"},{"key":"637_CR11","unstructured":"Kragl, B., Qadeer, S., Henzinger, T.A.: Synchronizing the asynchronous. In: CONCUR, pp. 21:1\u201321:17 (2018)"},{"key":"637_CR12","doi-asserted-by":"crossref","unstructured":"Bakst, A., von Gleissenthall, K., Kici, R.G., Jhala, R.: Verifying distributed programs via canonical sequentialization. In: PACMPL 1(OOPSLA), 110:1-110:27 (2017)","DOI":"10.1145\/3133934"},{"key":"637_CR13","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: POPL, pp. 719\u2013734 (2017)","DOI":"10.1145\/3093333.3009860"},{"key":"637_CR14","doi-asserted-by":"publisher","unstructured":"Gleissenthall, K.V., Kici, R.G., Bakst, A., Stefan, D., Jhala, R.: Pretend synchrony: synchronous verification of asynchronous distributed programs. Proc. ACM Program. Lang. 3(POPL), 59:1\u201359:30 (2019). https:\/\/doi.org\/10.1145\/3290372","DOI":"10.1145\/3290372"},{"issue":"1","key":"637_CR15","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1109\/2.248873","volume":"27","author":"H Kopetz","year":"1994","unstructured":"Kopetz, H., Gr\u00fcnsteidl, G.: TTP - a protocol for fault-tolerant real-time systems. IEEE Computer 27(1), 14\u201323 (1994)","journal-title":"IEEE Computer"},{"issue":"3","key":"637_CR16","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1016\/0167-6423(83)90013-8","volume":"2","author":"T Elrad","year":"1982","unstructured":"Elrad, T., Francez, N.: Decomposition of distributed programs into communication-closed layers. Sci. Comput. Progr. 2(3), 155\u2013173 (1982)","journal-title":"Sci. Comput. Progr."},{"key":"637_CR17","doi-asserted-by":"crossref","unstructured":"Chou, C., Gafni, E.: Understanding and verifying distributed algorithms using stratified decomposition. In: PODC, pp. 44\u201365 (1988)","DOI":"10.1145\/62546.62556"},{"key":"637_CR18","doi-asserted-by":"crossref","unstructured":"Chaouch-Saad, M., Charron-Bost, B., Merz, S.: A reduction theorem for the verification of round-based distributed algorithms. In: RP, LNCS 5797, 93\u2013106 (2009)","DOI":"10.1007\/978-3-642-04420-5_10"},{"key":"637_CR19","doi-asserted-by":"crossref","unstructured":"Damian, A., Dragoi, C., Militaru, A., Widder, J.: Communication-closed asynchronous protocols. In: Computer Aided Verification - 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part II, pp. 344\u2013363 (2019). https:\/\/doi.org\/10.1007\/978-3-030-25543-5_20","DOI":"10.1007\/978-3-030-25543-5_20"},{"key":"637_CR20","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/j.ic.2016.03.006","volume":"252","author":"IV Konnov","year":"2017","unstructured":"Konnov, I.V., Veith, H., Widder, J.: On the completeness of bounded model checking for threshold-based distributed algorithms: reachability. Inf. Comput. 252, 95\u2013109 (2017). https:\/\/doi.org\/10.1016\/j.ic.2016.03.006","journal-title":"Inf. Comput."},{"key":"637_CR21","unstructured":"Lazi\u0107, M., Konnov, I., Widder, J., Bloem, R.: Synthesis of Distributed Algorithms with Parameterized Threshold Guards. In: OPODIS, LIPIcs 95, pp. 32:1\u201332:20 (2017)"},{"issue":"2","key":"637_CR22","doi-asserted-by":"publisher","first-page":"374","DOI":"10.1145\/3149.214121","volume":"32","author":"MJ Fischer","year":"1985","unstructured":"Fischer, M.J., Lynch, N.A., Paterson, M.S.: Impossibility of distributed consensus with one faulty process. J. ACM 32(2), 374\u2013382 (1985)","journal-title":"J. ACM"},{"key":"637_CR23","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. Dist. Comp. 2, 80\u201394 (1987)","journal-title":"Dist. Comp."},{"key":"637_CR24","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic Model Checking without BDDs. In: TACAS, LNCS 1579, 193\u2013207 (1999)","DOI":"10.1007\/3-540-49059-0_14"},{"key":"637_CR25","doi-asserted-by":"crossref","unstructured":"Kroening, D., Strichman, O.: Efficient Computation of Recurrence Diameters. In: VMCAI, LNCS 2575, pp. 298\u2013309 (2003)","DOI":"10.1007\/3-540-36384-X_24"},{"key":"637_CR26","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Kroening, D., Ouaknine, J., Strichman, O.: Completeness and complexity of bounded model checking. In: VMCAI, LNCS 2937, 85\u201396 (2004)","DOI":"10.1007\/978-3-540-24622-0_9"},{"key":"637_CR27","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: TACAS, pp. 337\u2013340 (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"637_CR28","doi-asserted-by":"crossref","unstructured":"Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanovic, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: CAV, pp. 171\u2013177 (2011)","DOI":"10.1007\/978-3-642-22110-1_14"},{"issue":"40","key":"637_CR29","doi-asserted-by":"publisher","first-page":"5602","DOI":"10.1016\/j.tcs.2010.09.032","volume":"412","author":"M Biely","year":"2011","unstructured":"Biely, M., Schmid, U., Weiss, B.: Synchronous consensus under hybrid process and link failures. Theor. Comput. Sci. 412(40), 5602\u20135630 (2011)","journal-title":"Theor. Comput. Sci."},{"key":"637_CR30","doi-asserted-by":"crossref","unstructured":"Berman, P., Garay, J.A., Perry, K.J.: Towards optimal distributed consensus (Extended Abstract). In: FOCS, pp. 410\u2013415 (1989)","DOI":"10.1109\/SFCS.1989.63511"},{"key":"637_CR31","doi-asserted-by":"crossref","unstructured":"Berman, P., Garay, J.A., Perry, K.J.: Asymptotically Optimal Distributed Consensus. Tech. rep., Bell Labs (1989)","DOI":"10.1109\/SFCS.1989.63511"},{"key":"637_CR32","volume-title":"Distributed Algorithms","author":"N Lynch","year":"1996","unstructured":"Lynch, N.: Distributed Algorithms. Morgan Kaufman, Massachusetts (1996)"},{"issue":"5","key":"637_CR33","doi-asserted-by":"publisher","first-page":"912","DOI":"10.1145\/355483.355489","volume":"47","author":"S Chaudhuri","year":"2000","unstructured":"Chaudhuri, S., Herlihy, M., Lynch, N.A., Tuttle, M.R.: Tight bounds for k-set agreement. J. ACM 47(5), 912\u2013943 (2000)","journal-title":"J. ACM"},{"key":"637_CR34","series-title":"Synthesis Lectures on Distributed Computing Theory","doi-asserted-by":"publisher","DOI":"10.2200\/S00294ED1V01Y201009DCT003","volume-title":"Fault-Tolerant Agreement in Synchronous Message-Passing Systems","author":"M Raynal","year":"2010","unstructured":"Raynal, M.: Fault-Tolerant Agreement in Synchronous Message-Passing Systems. Synthesis Lectures on Distributed Computing Theory, Morgan & Claypool Publishers, California (2010)"},{"key":"637_CR35","doi-asserted-by":"crossref","unstructured":"Aminof, B., Rubin, S., Stoilkovska, I., Widder, J., Zuleger, F.: Parameterized model checking of synchronous distributed algorithms by abstraction. In: VMCAI, LNCS, vol. 10747, pp. 1\u201324. Springer (2018)","DOI":"10.1007\/978-3-319-73721-8_1"},{"key":"637_CR36","volume-title":"Computation: Finite and Infinite Machines","author":"ML Minsky","year":"1967","unstructured":"Minsky, M.L.: Computation: Finite and Infinite Machines. Prentice-Hall Inc, Upper Saddle River (1967)"},{"key":"637_CR37","series-title":"Synthesis Lectures on Distributed Computing Theory","doi-asserted-by":"publisher","DOI":"10.2200\/S00658ED1V01Y201508DCT013","volume-title":"Decidability of Parameterized Verification","author":"R Bloem","year":"2015","unstructured":"Bloem, R., Jacobs, S., Khalimov, A., Konnov, I., Rubin, S., Veith, H., Widder, J.: Decidability of Parameterized Verification. Synthesis Lectures on Distributed Computing Theory, Morgan & Claypool Publishers, California (2015)"},{"issue":"4","key":"637_CR38","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. Int. J. Found. Comput. Sci. 14(4), 527\u2013550 (2003)","journal-title":"Int. J. Found. Comput. Sci."},{"key":"637_CR39","doi-asserted-by":"crossref","unstructured":"Konnov, I., Veith, H., Widder, J.: SMT and POR beat counter abstraction: parameterized model checking of threshold-based distributed algorithms. In: CAV (Part\u00a0I), LNCS, vol. 9206, pp. 85\u2013102 (2015)","DOI":"10.1007\/978-3-319-21690-4_6"},{"key":"637_CR40","unstructured":"Experiments. https:\/\/github.com\/istoilkovska\/syncTA"},{"issue":"3","key":"637_CR41","doi-asserted-by":"publisher","first-page":"500","DOI":"10.1007\/s10703-017-0290-y","volume":"51","author":"A Reynolds","year":"2017","unstructured":"Reynolds, A., King, T., Kuncak, V.: Solving quantified linear arithmetic by counterexample-guided instantiation. Form. Methods Syst. Des. 51(3), 500\u2013532 (2017)","journal-title":"Form. Methods Syst. Des."},{"key":"637_CR42","unstructured":"Bj\u00f8rner, N., Janota, M.: Playing with quantified satisfaction. In: A.\u00a0Fehnker, A.\u00a0McIver, G.\u00a0Sutcliffe, A.\u00a0Voronkov (eds.) 20th International Conferences on Logic for Programming, Artificial Intelligence and Reasoning - Short Presentations, LPAR 2015, Suva, Fiji, November 24-28, 2015, EPiC Series in Computing, vol.\u00a035, pp. 15\u201327. EasyChair (2015)"},{"key":"637_CR43","doi-asserted-by":"crossref","unstructured":"Mari\u0107, O., Sprenger, C., Basin, D.A.: cutoff bounds for consensus algorithms. In: CAV, pp. 217\u2013237 (2017)","DOI":"10.1007\/978-3-319-63390-9_12"},{"key":"637_CR44","unstructured":"Kukovec, J., Konnov, I., Widder, J.: Reachability in parameterized systems: all flavors of threshold automata. In: CONCUR, pp. 19:1\u201319:17 (2018)"},{"key":"637_CR45","doi-asserted-by":"publisher","unstructured":"Stoilkovska, I., Konnov, I., Widder, J., Zuleger, F.: Eliminating message counters in synchronous threshold automata. In: Henglein, F., Shoham, S., Vizel, Y. (eds.) Verification, Model Checking, and Abstract Interpretation\u201422nd International Conference, VMCAI 2021, Copenhagen, Denmark, 17\u201319 January 2021, Proceedings. Lecture Notes in Computer Science, vol. 12597, pp. 196\u2013218. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-67067-2_10","DOI":"10.1007\/978-3-030-67067-2_10"},{"key":"637_CR46","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Namjoshi, K.S.: Automatic verification of parameterized synchronous systems, In: CAV, LNCS, (ed.) vol. 1102, pp. 87\u201398. Springer (1996)","DOI":"10.1007\/3-540-61474-5_60"},{"key":"637_CR47","unstructured":"Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.: General decidability theorems for infinite-state systems. In: LICS, pp. 313\u2013321 (1996)"},{"key":"637_CR48","doi-asserted-by":"crossref","unstructured":"Aminof, B., Rubin, S., Zuleger, F., Spegni, F.: Liveness of parameterized timed networks. In: ICALP, pp. 375\u2013387 (2015)","DOI":"10.1007\/978-3-662-47666-6_30"},{"key":"637_CR49","doi-asserted-by":"crossref","unstructured":"Leroux, J., Sutre, G.: Flat Counter Automata Almost Everywhere! . In: ATVA, LNCS 3707, pp. 489\u2013503 (2005)","DOI":"10.1007\/11562948_36"},{"key":"637_CR50","doi-asserted-by":"crossref","unstructured":"Bardin, S., Leroux, J., Point, G.: FAST Extended Release. In: CAV, LNCS 4144, 63\u201366 (2006)","DOI":"10.1007\/11817963_9"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-021-00637-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10009-021-00637-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-021-00637-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,3,15]],"date-time":"2022-03-15T16:16:07Z","timestamp":1647360967000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10009-021-00637-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,8,30]]},"references-count":50,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2022,2]]}},"alternative-id":["637"],"URL":"https:\/\/doi.org\/10.1007\/s10009-021-00637-9","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,8,30]]},"assertion":[{"value":"30 August 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}