{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,8]],"date-time":"2026-06-08T07:00:31Z","timestamp":1780902031222,"version":"3.54.1"},"reference-count":70,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2026,6,1]],"date-time":"2026-06-01T00:00:00Z","timestamp":1780272000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,6,1]],"date-time":"2026-06-01T00:00:00Z","timestamp":1780272000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Theory Comput Syst"],"published-print":{"date-parts":[[2026,6]]},"DOI":"10.1007\/s00224-026-10283-w","type":"journal-article","created":{"date-parts":[[2026,6,8]],"date-time":"2026-06-08T06:41:58Z","timestamp":1780900918000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Cutoff Theorems for the Model Checking of Crash-Tolerant Causal Broadcast"],"prefix":"10.1007","volume":"70","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1545-127X","authenticated-orcid":false,"given":"Leila","family":"NamvariTazehkand","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8949-9180","authenticated-orcid":false,"given":"Saeid","family":"Pashazadeh","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5266-1087","authenticated-orcid":false,"given":"Ali","family":"Ebnenasir","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,6,8]]},"reference":[{"key":"10283_CR1","doi-asserted-by":"publisher","first-page":"105837","DOI":"10.1016\/j.ipl.2019.105837","volume":"151","author":"A Mostefaoui","year":"2019","unstructured":"Mostefaoui, A., Perrin, M., Raynal, M., Cao, J.: Crash-tolerant causal broadcast in o(n) messages. Inf. Process. Lett. 151, 105837 (2019). https:\/\/doi.org\/10.1016\/j.ipl.2019.105837","journal-title":"Inf. Process. Lett."},{"key":"10283_CR2","unstructured":"Lamport, L.: Time, clocks, and the ordering of events in a distributed system. In: Concurrency: the Works of Leslie Lamport, pp. 179\u2013196 (2019)"},{"key":"10283_CR3","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1016\/j.tcs.2021.07.004","volume":"885","author":"A Auvolat","year":"2021","unstructured":"Auvolat, A., Frey, D., Raynal, M., Ta\u00efani, F.: Byzantine-tolerant causal broadcast. Theoret. Comput. Sci. 885, 55\u201368 (2021). https:\/\/doi.org\/10.1016\/j.tcs.2021.07.004","journal-title":"Theoret. Comput. Sci."},{"key":"10283_CR4","doi-asserted-by":"crossref","unstructured":"Ravindran, K., Shah, K.: Causal broadcasting and consistency of distributed shared data. In: 14th International Conference on Distributed Computing Systems, pp. 40\u201347 (1994). IEEE","DOI":"10.1109\/ICDCS.1994.302390"},{"key":"10283_CR5","doi-asserted-by":"crossref","unstructured":"N\u00e9delec, B., Molli, P., Mostefaoui, A.: Crate: Writing stories together with our browsers. In: Proceedings of the 25th International Conference Companion on World Wide Web, pp. 231\u2013234 (2016)","DOI":"10.1145\/2872518.2890539"},{"key":"10283_CR6","doi-asserted-by":"crossref","unstructured":"Heinrich, M., Lehmann, F., Springer, T., Gaedke, M.: Exploiting single-user web applications for shared editing: a generic transformation approach. In: Proceedings of the 21st International Conference on World Wide Web, pp. 1057\u20131066 (2012)","DOI":"10.1145\/2187836.2187978"},{"issue":"1","key":"10283_CR7","doi-asserted-by":"publisher","first-page":"8","DOI":"10.1145\/43921.43922","volume":"22","author":"A Demers","year":"1988","unstructured":"Demers, A., Greene, D., Houser, C., Irish, W., Larson, J., Shenker, S., Sturgis, H., Swinehart, D., Terry, D.: Epidemic algorithms for replicated database maintenance. ACM SIGOPS Operating Systems Review 22(1), 8\u201332 (1988). https:\/\/doi.org\/10.1145\/43921.43922","journal-title":"ACM SIGOPS Operating Systems Review"},{"key":"10283_CR8","doi-asserted-by":"crossref","unstructured":"Bailis, P., Ghodsi, A., Hellerstein, J.M., Stoica, I.: Bolt-on causal consistency. In: Proceedings of the 2013 ACM SIGMOD International Conference on Management of Data, pp. 761\u2013772 (2013)","DOI":"10.1145\/2463676.2465279"},{"key":"10283_CR9","doi-asserted-by":"publisher","unstructured":"Bravo, M., Rodrigues, L., Van\u00a0Roy, P.: Saturn: a distributed metadata service for causal consistency. In: Proceedings of the 12th European Conference on Computer Systems, pp. 111\u2013126 (2017). https:\/\/doi.org\/10.1145\/3064176.3064210","DOI":"10.1145\/3064176.3064210"},{"key":"10283_CR10","doi-asserted-by":"publisher","unstructured":"Borthakur, D.: Petabyte scale databases and storage systems at facebook. In: Proceedings of the 2013 ACM SIGMOD International Conference on Management of Data, pp. 1267\u20131268 (2013). https:\/\/doi.org\/10.1145\/2463676.2467796","DOI":"10.1145\/2463676.2467796"},{"key":"10283_CR11","doi-asserted-by":"publisher","unstructured":"Wilhelm, D., Arantes, L., Sens, P.: A scalable causal broadcast that tolerates dynamics of mobile networks. In: Proceedings of the 23rd International Conference on Distributed Computing and Networking, pp. 9\u201318 (2022). https:\/\/doi.org\/10.1145\/3491003.3491014","DOI":"10.1145\/3491003.3491014"},{"key":"10283_CR12","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/j.future.2021.01.004","volume":"118","author":"F Guidec","year":"2021","unstructured":"Guidec, F., Launay, P., Mah\u00e9o, Y.: Causal and $$\\delta $$-causal broadcast in opportunistic networks. Futur. Gener. Comput. Syst. 118, 142\u2013156 (2021). https:\/\/doi.org\/10.1016\/j.future.2021.01.004","journal-title":"Futur. Gener. Comput. Syst."},{"key":"10283_CR13","doi-asserted-by":"crossref","unstructured":"Redmond, P., Shen, G., Vazou, N., Kuper, L.: Verified causal broadcast with liquid haskell (2022). arXiv preprint arXiv:2206.14767","DOI":"10.1145\/3587216.3587222"},{"issue":"1","key":"10283_CR14","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1145\/2914770.2837622","volume":"51","author":"M Lesani","year":"2016","unstructured":"Lesani, M., Bell, C.J., Chlipala, A.: Chapar: certified causally consistent distributed key-value stores. ACM SIGPLAN Notices 51(1), 357\u2013370 (2016). https:\/\/doi.org\/10.1145\/2914770.2837622","journal-title":"ACM SIGPLAN Notices"},{"key":"10283_CR15","doi-asserted-by":"crossref","unstructured":"Paulin-Mohring, C.: Introduction to the coq proof-assistant for practical software verification. In: Tools for Practical Software Verification: LASER, International Summer School 2011, Elba Island, Italy, Revised Tutorial Lectures, pp. 45\u201395 (2012)","DOI":"10.1007\/978-3-642-35746-6_3"},{"key":"10283_CR16","doi-asserted-by":"publisher","unstructured":"Liu, Y., Parker, J., Redmond, P., Kuper, L., Hicks, M., Vazou, N.: Verifying replicated data types with type class refinements in liquid haskell. Proceedings of the ACM on Programming Languages 4(OOPSLA), pp. 1\u201330 (2020). https:\/\/doi.org\/10.1145\/3428284","DOI":"10.1145\/3428284"},{"key":"10283_CR17","doi-asserted-by":"publisher","unstructured":"Gondelman, L., Gregersen, S.O., Nieto, A., Timany, A., Birkedal, L.: Distributed causal memory: modular specification and verification in higher-order distributed separation logic. In: Proceedings of the ACM on Programming Languages 5(POPL), 1\u201329 (2021). https:\/\/doi.org\/10.1145\/3434323","DOI":"10.1145\/3434323"},{"key":"10283_CR18","doi-asserted-by":"publisher","unstructured":"Bouajjani, A., Enea, C., Guerraoui, R., Hamza, J.: On verifying causal consistency. In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, pp. 626\u2013638 (2017). https:\/\/doi.org\/10.1145\/3009837.3009888","DOI":"10.1145\/3009837.3009888"},{"key":"10283_CR19","doi-asserted-by":"crossref","unstructured":"Zennou, R., Biswas, R., Bouajjani, A., Enea, C., Erradi, M.: Checking causal consistency of distributed databases. In: International Conference on Networked Systems, pp. 35\u201351 (2019). Springer","DOI":"10.1007\/978-3-030-31277-0_3"},{"key":"10283_CR20","doi-asserted-by":"crossref","unstructured":"Yadav, P., Suryavanshi, R., Yadav, D.: Formal verification of liveness properties in causal order broadcast systems using event-b. In: Proceedings of 2nd Doctoral Symposium on Computational Intelligence: DoSCI 2021, pp. 199\u2013210 (2021). Springer","DOI":"10.1007\/978-981-16-3346-1_16"},{"key":"10283_CR21","doi-asserted-by":"crossref","unstructured":"Yadav, P., Suryavanshi, R., Singh, A.K., Yadav, D.: Formal verification of causal order-based load distribution mechanism using event-b. In: Data, Engineering and Applications: Volume 2, pp. 229\u2013241 (2019)","DOI":"10.1007\/978-981-13-6351-1_18"},{"key":"10283_CR22","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1007\/s10009-010-0145-y","volume":"12","author":"J-R Abrial","year":"2010","unstructured":"Abrial, J.-R., Butler, M., Hallerstede, S., Hoang, T.S., Mehta, F., Voisin, L.: Rodin: an open toolset for modelling and reasoning in event-b. Int. J. Softw. Tools Technol. Transfer 12, 447\u2013466 (2010)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"10283_CR23","doi-asserted-by":"publisher","unstructured":"Fulmare, N., Yadav, D.: Rigorous analysis of byzantine causal order using event-b. In: Proceedings of the International Conference and Workshop on Emerging Trends in Technology, pp. 723\u2013726 (2010). https:\/\/doi.org\/10.1145\/1741906.1742074","DOI":"10.1145\/1741906.1742074"},{"key":"10283_CR24","unstructured":"Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual vol. 1003, (2004). Addison-Wesley Reading"},{"key":"10283_CR25","doi-asserted-by":"crossref","unstructured":"Tran, T.-H., Konnov, I., Widder, J.: Cutoffs for symmetric point-to-point distributed algorithms. In: International Conference on Networked Systems, pp. 329\u2013346 (2020). Springer","DOI":"10.1007\/978-3-030-67087-0_21"},{"key":"10283_CR26","unstructured":"Holzmann, G.J.: Promela language reference. http:\/\/spinroot.com\/spin\/Man\/promela.html. Accessed 07 Jul 2024"},{"key":"10283_CR27","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Symbolic model checking. In: Symbolic Model Checking, pp. 25\u201360 (1993). Springer","DOI":"10.1007\/978-1-4615-3190-6_3"},{"issue":"5","key":"10283_CR28","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"GJ Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The model checker spin. IEEE Trans. Software Eng. 23(5), 279\u2013295 (1997)","journal-title":"IEEE Trans. Software Eng."},{"key":"10283_CR29","doi-asserted-by":"crossref","unstructured":"NamvariTazehkand, L., Ebnenasir, A.: A novel approach for specification and verification of symmetric distributed algorithms using spin. In: 2024 3rd International Conference on Distributed Computing and High Performance Computing (DCHPC), pp. 1\u20139 (2024). IEEE","DOI":"10.1109\/DCHPC60845.2024.10454070"},{"key":"10283_CR30","doi-asserted-by":"crossref","unstructured":"NamvariTazehkand, L., Ebnenasir, A., Pashazadeh, S.: Model Checking of a Causal Broadcast Algorithm Using Spin. Mendeley Data (2023). https:\/\/data.mendeley.com\/datasets\/ptznpn848p\/1","DOI":"10.1109\/DCHPC60845.2024.10454067"},{"key":"10283_CR31","doi-asserted-by":"crossref","unstructured":"NamvariTazehkand, L., Ebnenasir, A., Pashazadeh, S.: Modeling and Verifying a Crash-Tolerant Causal Broadcast Algorithm Using SPIN. Mendeley Data (2024). https:\/\/data.mendeley.com\/datasets\/v4gvjzc3mw\/1","DOI":"10.1109\/DCHPC60845.2024.10454067"},{"issue":"1","key":"10283_CR32","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1145\/7351.7478","volume":"5","author":"KP Birman","year":"1987","unstructured":"Birman, K.P., Joseph, T.A.: Reliable communication in the presence of failures. ACM Transactions on Computer Systems (TOCS) 5(1), 47\u201376 (1987)","journal-title":"ACM Transactions on Computer Systems (TOCS)"},{"issue":"2","key":"10283_CR33","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1145\/122120.122133","volume":"25","author":"K Birman","year":"1991","unstructured":"Birman, K., Cooper, R.: The isis project: Real experience with a fault tolerant programming system. ACM SIGOPS Operating Systems Review 25(2), 103\u2013107 (1991)","journal-title":"ACM SIGOPS Operating Systems Review"},{"key":"10283_CR34","doi-asserted-by":"publisher","first-page":"923","DOI":"10.1007\/s00607-015-0479-0","volume":"98","author":"R Juan-Mar\u00edn","year":"2016","unstructured":"Juan-Mar\u00edn, R., Decker, H., Armend\u00e1riz-\u00cdnigo, J.E., Bernab\u00e9u-Aub\u00e1n, J.M., Mu\u00f1oz-Esco\u00ed, F.D.: Scalability approaches for causal multicast: a survey. Computing 98, 923\u2013947 (2016). https:\/\/doi.org\/10.1007\/s00607-015-0479-0","journal-title":"Computing"},{"key":"10283_CR35","unstructured":"Juan, R., Decker, H., Miedes, E., Armend\u00e1riz, J., Munoz, F.: A survey of scalability approaches for reliable causal broadcasts. Technical report, Tech. Rep. ITI-SIDI-2009\/010 (2009)"},{"key":"10283_CR36","doi-asserted-by":"crossref","unstructured":"Gambhire, P., Kshemkalyani, A.D.: Reducing false causality in causal message ordering. In: International Conference on High-Performance Computing, pp. 61\u201372 (2000). Springer","DOI":"10.1007\/3-540-44467-X_6"},{"key":"10283_CR37","doi-asserted-by":"crossref","unstructured":"Cachin, C., Guerraoui, R., Rodrigues, L.: Introduction to Reliable and Secure Distributed Programming, (2011). Springer Science & Business Media","DOI":"10.1007\/978-3-642-15260-3"},{"issue":"6","key":"10283_CR38","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1016\/0020-0190(91)90008-6","volume":"39","author":"M Raynal","year":"1991","unstructured":"Raynal, M., Schiper, A., Toueg, S.: The causal ordering abstraction and a simple way to implement it. Inf. Process. Lett. 39(6), 343\u2013350 (1991). https:\/\/doi.org\/10.1016\/0020-0190(91)90008-6","journal-title":"Inf. Process. Lett."},{"issue":"2","key":"10283_CR39","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/s004460050044","volume":"11","author":"AD Kshemkalyani","year":"1998","unstructured":"Kshemkalyani, A.D., Singhal, M.: Necessary and sufficient conditions on information for causal message ordering and their optimal implementation. Distrib. Comput. 11(2), 91\u2013111 (1998). https:\/\/doi.org\/10.1007\/s004460050044","journal-title":"Distrib. Comput."},{"key":"10283_CR40","doi-asserted-by":"publisher","unstructured":"Misra, A., Kshemkalyani, A.D.: Byzantine fault-tolerant causal ordering. In: 24th International Conference on Distributed Computing and Networking, pp. 100\u2013109 (2023). https:\/\/doi.org\/10.1145\/3571306.3571395","DOI":"10.1145\/3571306.3571395"},{"key":"10283_CR41","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1023\/A:1013613607398","volume":"2","author":"L-H Yen","year":"1997","unstructured":"Yen, L.-H., Huang, T.-L., Hwang, S.-Y.: A protocol for causally ordered message delivery in mobile computing systems. Mobile Networks and Applications 2, 365\u2013372 (1997). https:\/\/doi.org\/10.1023\/A:1013613607398","journal-title":"Mobile Networks and Applications"},{"key":"10283_CR42","doi-asserted-by":"crossref","unstructured":"N\u00e9delec, B., Molli, P., Most\u00e9faoui, A.: Breaking the scalability barrier of causal broadcast for large and dynamic systems. In: 2018 IEEE 37th Symposium on Reliable Distributed Systems (SRDS), pp. 51\u201360 (2018). IEEE","DOI":"10.1109\/SRDS.2018.00016"},{"key":"10283_CR43","doi-asserted-by":"crossref","unstructured":"Chandra, P., Kshemkalyani, A.D.: Causal multicast in mobile networks. In: The IEEE Computer Society\u2019s 12th Annual International Symposium on Modeling, Analysis, and Simulation of Computer and Telecommunications Systems (MASCOTS 2004), pp. 213\u2013220 (2004). IEEE","DOI":"10.1109\/MASCOT.2004.1348235"},{"key":"10283_CR44","doi-asserted-by":"crossref","unstructured":"Benzaid, C., Badache, N.: An optimal causal broadcast protocol in mobile dynamic groups. In: 2008 IEEE International Symposium on Parallel and Distributed Processing with Applications, pp. 477\u2013484 (2008). IEEE","DOI":"10.1109\/ISPA.2008.36"},{"issue":"1","key":"10283_CR45","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1016\/j.future.2003.07.013","volume":"20","author":"Y Zeng","year":"2004","unstructured":"Zeng, Y., Cai, W., Turner, S.J., Zhou, S., Lee, B.-S.: Characterization and delivery of directly coupled causal messages in distributed systems. Futur. Gener. Comput. Syst. 20(1), 171\u2013178 (2004). https:\/\/doi.org\/10.1016\/j.future.2003.07.013","journal-title":"Futur. Gener. Comput. Syst."},{"key":"10283_CR46","doi-asserted-by":"publisher","first-page":"1118","DOI":"10.1016\/j.future.2017.04.044","volume":"86","author":"T-Y Hsu","year":"2018","unstructured":"Hsu, T.-Y., Kshemkalyani, A.D., Shen, M.: Causal consistency algorithms for partially replicated and fully replicated systems. Futur. Gener. Comput. Syst. 86, 1118\u20131133 (2018). https:\/\/doi.org\/10.1016\/j.future.2017.04.044","journal-title":"Futur. Gener. Comput. Syst."},{"issue":"3","key":"10283_CR47","doi-asserted-by":"publisher","first-page":"527","DOI":"10.1109\/TPDS.2020.3026778","volume":"32","author":"K Spirovska","year":"2020","unstructured":"Spirovska, K., Didona, D., Zwaenepoel, W.: Optimistic causal consistency for geo-replicated key-value stores. IEEE Trans. Parallel Distrib. Syst. 32(3), 527\u2013542 (2020)","journal-title":"IEEE Trans. Parallel Distrib. Syst."},{"key":"10283_CR48","doi-asserted-by":"crossref","unstructured":"Misra, A., Kshemkalyani, A.D.: Solvability of byzantine fault-tolerant causal ordering problems. In: International Conference on Networked Systems, pp. 87\u2013103 (2022). Springer","DOI":"10.1007\/978-3-031-17436-0_7"},{"key":"10283_CR49","doi-asserted-by":"crossref","unstructured":"Misra, A., Kshemkalyani, A.D.: Causal ordering properties of byzantine reliable broadcast primitives. In: 2022 IEEE 21st International Symposium on Network Computing and Applications (NCA), vol. 21, pp. 115\u2013122 (2022). IEEE","DOI":"10.1109\/NCA57778.2022.10013634"},{"key":"10283_CR50","doi-asserted-by":"crossref","unstructured":"Misra, A., Kshemkalyani, A.D.: Detecting causality in the presence of byzantine processes: There is no holy grail. In: 2022 IEEE 21st International Symposium on Network Computing and Applications (NCA), vol. 21, pp. 73\u201380 (2022). IEEE","DOI":"10.1109\/NCA57778.2022.10013644"},{"key":"10283_CR51","doi-asserted-by":"crossref","unstructured":"Misra, A., Kshemkalyani, A.D.: Byzantine fault-tolerant causal broadcast on incomplete graphs. In: 2022 IEEE 21st International Symposium on Network Computing and Applications (NCA), vol. 21, pp. 63\u201371 (2022). IEEE","DOI":"10.1109\/NCA57778.2022.10013642"},{"key":"10283_CR52","doi-asserted-by":"publisher","DOI":"10.1109\/TPDS.2024.3368280","author":"A Misra","year":"2024","unstructured":"Misra, A., Kshemkalyani, A.D.: Byzantine-tolerant causal ordering for unicasts, multicasts, and broadcasts. IEEE Trans. Parallel Distrib. Syst. (2024). https:\/\/doi.org\/10.1109\/TPDS.2024.3368280","journal-title":"IEEE Trans. Parallel Distrib. Syst."},{"key":"10283_CR53","unstructured":"Yadav, D., Butler, M.: Formal specifications and verification of message ordering properties in a broadcasting system using event-b. (2007)"},{"key":"10283_CR54","first-page":"8887","volume":"975","author":"R Suryavanshi","year":"2011","unstructured":"Suryavanshi, R., Yadav, D.: Rigorous design of partition-aware total order broadcast system using event-b. Int. J. Comput. Appl. 975, 8887 (2011)","journal-title":"Int. J. Comput. Appl."},{"key":"10283_CR55","doi-asserted-by":"crossref","unstructured":"Mosbahi, O., Jaray, J.: Specification and proof of liveness properties in b event systems. In: 2nd International Conference on Software and Data Technologies-ICSOFT 2007, pp. 25\u201334 (2007). INSTICC Press","DOI":"10.5220\/0001342400250034"},{"key":"10283_CR56","unstructured":"Pe\u00f1a, R.: An introduction to liquid haskell (2017). arXiv preprint arXiv:1701.03320"},{"key":"10283_CR57","unstructured":"Hoang, T.S.: An introduction to the event-b modelling method. In: Industrial Deployment of System Engineering Methods, pp. 211\u2013236 (2013)"},{"key":"10283_CR58","doi-asserted-by":"publisher","unstructured":"Raynal, M.: Distributed Algorithms for Message-passing Systems vol. 500. Springer(2013). https:\/\/doi.org\/10.1007\/978-3-642-38123-2","DOI":"10.1007\/978-3-642-38123-2"},{"key":"10283_CR59","doi-asserted-by":"crossref","unstructured":"Nieto, A., Gondelman, L., Reynaud, A., Timany, A., Birkedal, L.: Modular verification of op-based crdts in separation logic. In: Proceedings of the ACM on Programming Languages 6(OOPSLA2), 1788\u20131816 (2022)","DOI":"10.1145\/3563351"},{"key":"10283_CR60","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Kahlon, V.: Reducing model checking of the many to the few. In: International Conference on Automated Deduction, pp. 236\u2013254 (2000). Springer","DOI":"10.1007\/10721959_19"},{"key":"10283_CR61","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Kahlon, V.: Exact and efficient verification of parameterized cache coherence protocols. In: Advanced Research Working Conference on Correct Hardware Design and Verification Methods, pp. 247\u2013262 (2003). Springer","DOI":"10.1007\/978-3-540-39724-3_22"},{"issue":"04","key":"10283_CR62","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(04), 527\u2013549 (2003)","journal-title":"Int. J. Found. Comput. Sci."},{"key":"10283_CR63","doi-asserted-by":"crossref","unstructured":"Mari\u0107, O., Sprenger, C., Basin, D.: Cutoff bounds for consensus algorithms. In: International Conference on Computer Aided Verification, pp. 217\u2013237 (2017). Springer","DOI":"10.1007\/978-3-319-63390-9_12"},{"issue":"11","key":"10283_CR64","doi-asserted-by":"publisher","first-page":"4447","DOI":"10.1109\/TSE.2021.3119771","volume":"48","author":"A Ebnenasir","year":"2021","unstructured":"Ebnenasir, A.: Verification and synthesis of responsive symmetric uni-rings. IEEE Trans. Software Eng. 48(11), 4447\u20134464 (2021)","journal-title":"IEEE Trans. Software Eng."},{"key":"10283_CR65","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1016\/j.tcs.2019.12.026","volume":"813","author":"L Spalazzi","year":"2020","unstructured":"Spalazzi, L., Spegni, F.: Parameterized model checking of networks of timed automata with boolean guards. Theoret. Comput. Sci. 813, 248\u2013269 (2020). https:\/\/doi.org\/10.1016\/j.tcs.2019.12.026","journal-title":"Theoret. Comput. Sci."},{"key":"10283_CR66","volume-title":"An introduction to input\/output automata","author":"NA Lynch","year":"1988","unstructured":"Lynch, N.A., Tuttle, M.R.: An introduction to input\/output automata. Technical report, Laboratory for Computer Science, Massachusetts Institute of Technology (1988)"},{"key":"10283_CR67","unstructured":"Garland, S.J., Lynch, N.A.: Using i\/o automata for developing distributed systems. In: Foundations of Component-based Systems vol. 13, pp. 5\u20132 (2000)"},{"key":"10283_CR68","doi-asserted-by":"crossref","unstructured":"Liu, S., \u00d6lveczky, P.C., Zhang, M., Wang, Q., Meseguer, J.: Automatic analysis of consistency properties of distributed transaction systems in maude. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 40\u201357 (2019). Springer","DOI":"10.1007\/978-3-030-17465-1_3"},{"key":"10283_CR69","doi-asserted-by":"crossref","unstructured":"Ghasemirad, S., Liu, S., Sprenger, C., Multazzu, L., Basin, D.: Veriso: Verifiable isolation guarantees for database transactions (2025). arXiv preprint arXiv:2503.06284","DOI":"10.14778\/3718057.3718065"},{"key":"10283_CR70","doi-asserted-by":"crossref","unstructured":"Ghasemirad, S., Sprenger, C., Liu, S., Multazzu, L., Basin, D.: Pushing the limit: Verified performance-optimal causally-consistent database transactions. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 43\u201362 (2025). Springer","DOI":"10.1007\/978-3-031-90660-2_3"}],"container-title":["Theory of Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00224-026-10283-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00224-026-10283-w","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00224-026-10283-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,8]],"date-time":"2026-06-08T06:42:31Z","timestamp":1780900951000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s00224-026-10283-w"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,6]]},"references-count":70,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2026,6]]}},"alternative-id":["10283"],"URL":"https:\/\/doi.org\/10.1007\/s00224-026-10283-w","relation":{},"ISSN":["1432-4350","1433-0490"],"issn-type":[{"value":"1432-4350","type":"print"},{"value":"1433-0490","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,6]]},"assertion":[{"value":"11 July 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"22 May 2026","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"8 June 2026","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare no competing interests.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Competing interests"}},{"value":"This manuscript has not been submitted to, nor is under review at, another journal or other publishing venue.","order":3,"name":"Ethics","group":{"name":"EthicsHeading","label":"Submission Statement"}},{"value":"This article does not contain any studies involving human participants or animals performed by any of the authors.","order":4,"name":"Ethics","group":{"name":"EthicsHeading","label":"Ethical Approval"}}],"article-number":"38"}}