{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T12:12:17Z","timestamp":1781007137178,"version":"3.54.1"},"reference-count":37,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2021,2,24]],"date-time":"2021-02-24T00:00:00Z","timestamp":1614124800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,2,24]],"date-time":"2021-02-24T00:00:00Z","timestamp":1614124800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100001871","name":"Funda\u00e7\u00e3o para a Ci\u00eancia e a Tecnologia","doi-asserted-by":"publisher","award":["CISUC - UID\/CEC\/00326\/2020"],"award-info":[{"award-number":["CISUC - UID\/CEC\/00326\/2020"]}],"id":[{"id":"10.13039\/501100001871","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001871","name":"Funda\u00e7\u00e3o para a Ci\u00eancia e a Tecnologia","doi-asserted-by":"publisher","award":["P2020-31\/SI\/2017, No. 040004"],"award-info":[{"award-number":["P2020-31\/SI\/2017, No. 040004"]}],"id":[{"id":"10.13039\/501100001871","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Funda\u00e7\u00e3o para a Ci\u00eancia e a Tecnologia","award":["LASIGE - UIDB\/00408\/2020"],"award-info":[{"award-number":["LASIGE - UIDB\/00408\/2020"]}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Software Qual J"],"published-print":{"date-parts":[[2021,9]]},"DOI":"10.1007\/s11219-020-09539-6","type":"journal-article","created":{"date-parts":[[2021,2,24]],"date-time":"2021-02-24T15:04:24Z","timestamp":1614179064000},"page":"705-731","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Reductions and abstractions for formal verification of distributed round-based algorithms"],"prefix":"10.1007","volume":"29","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2916-7571","authenticated-orcid":false,"given":"Raul","family":"Barbosa","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Alcides","family":"Fonseca","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Filipe","family":"Araujo","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2021,2,24]]},"reference":[{"key":"9539_CR1","doi-asserted-by":"crossref","unstructured":"Aminof, B., Rubin, S., Stoilkovska, I., Widder, J., & Zuleger, F. (2018). Parameterized model checking of synchronous distributed algorithms by abstraction. In: International Conference on Verification, Model Checking, and Abstract Interpretation, Springer, pp. 1\u201324.","DOI":"10.1007\/978-3-319-73721-8_1"},{"key":"9539_CR2","doi-asserted-by":"publisher","unstructured":"Ben-Or, M. (1983). Another advantage of free choice (extended abstract): Completely asynchronous agreement protocols. In: Proceedings of the Second Annual ACM Symposium on Principles of Distributed Computing, Association for Computing Machinery, New York, NY, USA, PODC \u201983, pp. 27\u201330.\u00a0https:\/\/doi.org\/10.1145\/800221.806707","DOI":"10.1145\/800221.806707"},{"key":"9539_CR3","doi-asserted-by":"crossref","unstructured":"B\u00f3na, M. (2002). A walk through combinatorics: an introduction to enumeration and graph theory. World Scientific.","DOI":"10.1142\/4918"},{"key":"9539_CR4","doi-asserted-by":"publisher","unstructured":"Bondhugula, U., Hartono, A., Ramanujam, J., & Sadayappan, P. (2008). A practical automatic polyhedral parallelizer and locality optimizer. In: Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation, Tucson, AZ, USA, pp. 101\u2013113.\u00a0https:\/\/doi.org\/10.1145\/1375581.1375595","DOI":"10.1145\/1375581.1375595"},{"key":"9539_CR5","doi-asserted-by":"publisher","unstructured":"Bosnacki Dragan, D. D., & Holenderski, L. (2002). Symmetric spin. International Journal on Software Tools for Technology Transfer,4, 92\u2013106.\u00a0https:\/\/doi.org\/10.1007\/s100090200074","DOI":"10.1007\/s100090200074"},{"issue":"2","key":"9539_CR6","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"JR Burch","year":"1992","unstructured":"Burch, J. R., Clarke, E. M., McMillan, K. L., Dill, D. L., & Hwang, L. J. (1992). Symbolic model checking: 1020 states and beyond. Information and Computation, 98(2), 142\u2013170.","journal-title":"Information and Computation"},{"key":"9539_CR7","doi-asserted-by":"publisher","unstructured":"Chaouch-Saad, M., Charron-Bost, B., Merz, S. (2009). A reduction theorem for the verification of round-based distributed algorithms. In: Bournez O, Potapov I (eds) Reachability Problems, Lecture Notes in Computer Science, Springer Berlin Heidelberg, 5797,93\u2013106.\u00a0https:\/\/doi.org\/10.1007\/978-3-642-04420-5-10","DOI":"10.1007\/978-3-642-04420-5-10"},{"key":"9539_CR8","doi-asserted-by":"publisher","unstructured":"Charron-Bost, B., & Schiper, A. (2009). The heard-of model: computing in distributed systems with benign faults. Distributed Computing,22, 49\u201371.\u00a0https:\/\/doi.org\/10.1007\/s00446-009-0084-6","DOI":"10.1007\/s00446-009-0084-6"},{"key":"9539_CR9","doi-asserted-by":"publisher","unstructured":"Clarke, E., McMillan, K., Campos, S., Hartonas-Garmhausen, V. (1996). Symbolic model checking. In: Alur R, Henzinger T (eds) Computer Aided Verification, Lecture Notes in Computer Science, Springer Berlin Heidelberg, 1102,419\u2013422.\u00a0https:\/\/doi.org\/10.1007\/3-540-61474-5-93","DOI":"10.1007\/3-540-61474-5-93"},{"key":"9539_CR10","doi-asserted-by":"publisher","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., & Veith, H. (2000). Counterexampleguided abstraction refinement. In: Emerson E, Sistla A (eds) Computer Aided Verification, Lecture Notes in Computer Science, Springer Berlin Heidelberg, 1855,154\u2013169.\u00a0https:\/\/doi.org\/10.1007\/10722167_15","DOI":"10.1007\/10722167_15"},{"key":"9539_CR11","doi-asserted-by":"publisher","unstructured":"Clarke, E. M., Emerson, E. A., & Sistla, A. P. (1986). Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans Program Lang Syst,8(2), 244\u2013263. \nhttps:\/\/doi.org\/10.1145\/5397.5399","DOI":"10.1145\/5397.5399"},{"key":"9539_CR12","doi-asserted-by":"publisher","unstructured":"Clarke, E. M., Grumberg, O., & Long, D. E. (1994). Model checking and abstraction. ACM Trans Program Lang Syst,16(5), 15121542.\u00a0https:\/\/doi.org\/10.1145\/800221.806707","DOI":"10.1145\/800221.806707"},{"key":"9539_CR13","doi-asserted-by":"publisher","unstructured":"Clarke, E. M., Biere, A., Raimi, R., & Zhu, Y. (2001). Bounded model checking using satisfiability solving. Formal Methods in System Design,19(1), 7\u201334.\u00a0https:\/\/doi.org\/10.1023\/A:1011276507260","DOI":"10.1023\/A:1011276507260"},{"key":"9539_CR14","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds) (2018). Handbook of Model Checking. Springer.","DOI":"10.1007\/978-3-319-10575-8"},{"issue":"6","key":"9539_CR15","doi-asserted-by":"publisher","first-page":"642","DOI":"10.1109\/71.774912","volume":"10","author":"F Cristian","year":"1999","unstructured":"Cristian, F., & Fetzer, C. (1999). The timed asynchronous distributed system model. IEEE Transactions on Parallel and Distributed Systems,10(6), 642\u2013657.","journal-title":"IEEE Transactions on Parallel and Distributed Systems"},{"key":"9539_CR16","unstructured":"Dean, J., Sanjay Ghemawat, I., Google. (2004). Mapreduce: Simplified data processing on large clusters. In: Proceedings of the 6th Symposium on Operating Systems Design & Implementation (OSDI \u201904), Usenix."},{"key":"9539_CR17","doi-asserted-by":"publisher","unstructured":"Eisner, C., & Peled, D. (2002). Comparing symbolic and explicit model checking of a software system. Model Checking Software, Lecture Notes in Computer Science, Springer, Berlin Heidelberg,2318, 230\u2013239.\u00a0https:\/\/doi.org\/10.1007\/3-540-46017-9-18","DOI":"10.1007\/3-540-46017-9-18"},{"key":"9539_CR18","doi-asserted-by":"crossref","unstructured":"Elrad, T., & Francez, N. (1982). Decomposition of distributed programs into communication-closed layers. Science of Computer Programming,2(3), 55\u2013173.\u00a0http:\/\/www.sciencedirect.com\/science\/article\/pii\/0167642383900138","DOI":"10.1016\/0167-6423(83)90013-8"},{"key":"9539_CR19","doi-asserted-by":"publisher","unstructured":"Emerson, E., & Sistla, A. (1996). Symmetry and model checking. Formal Methods in System Design,9, 105131.\u00a0https:\/\/doi.org\/10.1007\/BF00625970","DOI":"10.1007\/BF00625970"},{"key":"9539_CR20","doi-asserted-by":"crossref","unstructured":"Erd\u0151s, P. (1942). On an elementary proof of some asymptotic formulas in the theory of partitions. Annals of Mathematics pp. 437\u2013450.","DOI":"10.2307\/1968802"},{"key":"9539_CR21","doi-asserted-by":"publisher","unstructured":"Fichte, J.K., Hecher, M., & Szeider, S. (2020). A time leap challenge for sat-solving. In: Simonis H (ed) Principles and Practice of Constraint Programming- 26th International Conference, CP 2020, Louvain-la-Neuve, Belgium,September 7-11, 2020, Proceedings, Springer, Lecture Notes in Computer Science, 12333,267\u2013285.\u00a0https:\/\/doi.org\/10.1007\/978-3-030-58475-7","DOI":"10.1007\/978-3-030-58475-7"},{"key":"9539_CR22","doi-asserted-by":"crossref","unstructured":"Gafni, E. (1998). Round-by-round fault detectors: Unifying synchrony and asynchrony (extended abstract). In: Coan BA, Afek Y (eds) Proceedings of the Seventeenth Annual ACM Symposium on Principles of Distributed Computing, PODC \u201998, Puerto Vallarta, Mexico, ACM, 143\u2013152.\u00a0http:\/\/dl.acm.org\/citation.cfm?id=277697","DOI":"10.1145\/277697.277724"},{"key":"9539_CR23","doi-asserted-by":"crossref","unstructured":"Garc\u00eda-P\u00e9rez, \u00c1., Gotsman, A., Meshman, Y., & Sergey, I. (2018). Paxos consensus, deconstructed and abstracted. European Symposium on Programming Cham: Springer, pp. 912\u2013939.","DOI":"10.1007\/978-3-319-89884-1_32"},{"issue":"1","key":"9539_CR24","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1112\/plms\/s2-17.1.75","volume":"2","author":"GH Hardy","year":"1918","unstructured":"Hardy, G. H., & Ramanujan, S. (1918). Asymptotic formula\u00e6in combinatory analysis. Proceedings of the London Mathematical Society,2(1), 75\u2013115.","journal-title":"Proceedings of the London Mathematical Society"},{"key":"9539_CR25","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1145\/114005.102808","volume":"13","author":"MP Herlihy","year":"1991","unstructured":"Herlihy, M. P. (1991). Wait-free synchronization. ACM Transactions on Programming Languages and Systems,13, 124\u2013149.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"9539_CR26","unstructured":"Holzmann, G. J. (2003). The SPIN Model Checker: primer and reference manual. Addison-Wesley."},{"key":"9539_CR27","volume-title":"Parallel and Distributed Programming Using C++","author":"C Hughes","year":"2003","unstructured":"Hughes, C., & Hughes, T. (2003). Parallel and Distributed Programming Using C++ (1st ed.). The address: Addison-Wesley.","edition":"1"},{"key":"9539_CR28","unstructured":"Lynch, N. (1996). Distributed Algorithms. Morgan Kaufmann, San Francisco, CS.\u00a0https:\/\/theory.lcs.mit.edu\/tds\/distalgs.html"},{"key":"9539_CR29","doi-asserted-by":"crossref","unstructured":"Mari\u0107, O., Sprenger, C., & Basin, D. (2017). Cutoff bounds for consensus algorithms. In: International Conference on Computer Aided Verification, Springer, 217\u2013237.","DOI":"10.1007\/978-3-319-63390-9_12"},{"key":"9539_CR30","doi-asserted-by":"crossref","unstructured":"Minsky, M. (1961). Recursive unsolvability of post\u2019s problem of \u201ctag\u201d and other topics in theory of turing machines. Annals of Mathematics,74, 437.","DOI":"10.2307\/1970290"},{"key":"9539_CR31","doi-asserted-by":"publisher","unstructured":"de Moura, L.M., & Bj\u00f8rner, N. (2008). Z3: an efficient SMT solver. In: Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, Proceedings, 337\u2013340.\u00a0https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"9539_CR32","doi-asserted-by":"publisher","unstructured":"Peled, D. (1994). Combining partial order reductions with on-the-y modelchecking. In: Dill D (ed) Computer Aided Verification, Lecture Notes in Computer Science, vol 818, Springer Berlin Heidelberg, 377\u2013390.\u00a0https:\/\/doi.org\/10.1007\/3-540-58179-0-69","DOI":"10.1007\/3-540-58179-0-69"},{"key":"9539_CR33","doi-asserted-by":"crossref","unstructured":"Raynal, M. (2018). Consensus and interactive consistency in synchronous systems prone to process crash failures. In: Fault-Tolerant Message-Passing Distributed Systems, Springer, 173\u2013187.","DOI":"10.1007\/978-3-319-94141-7_10"},{"key":"9539_CR34","doi-asserted-by":"crossref","unstructured":"Santoro, N., & Widmayer, P. (2005). Majority and unanimity in synchronous networks with ubiquitous dynamic faults. In: Pelc A, Raynal M (eds) Structural Information and Communication Complexity, 12th International Col-loquium, SIROCCO 2005, Mont Saint-Michel, France, Proceedings, Springer, Lecture Notes in Computer Science, 3499,262\u2013276.","DOI":"10.1007\/11429647_21"},{"key":"9539_CR35","doi-asserted-by":"crossref","unstructured":"Singh, G., P\u00fcschel, M., & Vechev, M.T. (2017). Fast polyhedra abstract domain. In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, 46\u201359.\u00a0http:\/\/dl.acm.org\/citation.cfm?id=3009885","DOI":"10.1145\/3009837.3009885"},{"key":"9539_CR36","doi-asserted-by":"publisher","unstructured":"Srikanth, T. K., & Toueg, S. (1987). Simulating authenticated broadcasts to derive simple fault-tolerant algorithms. Distrib Comput,2(2), 80\u201394.\u00a0https:\/\/doi.org\/10.1007\/BF01667080","DOI":"10.1007\/BF01667080"},{"key":"9539_CR37","doi-asserted-by":"publisher","unstructured":"Tsuchiya, T., & Schiper, A. (2008). Using bounded model checking to verify consensus algorithms. In: Taubenfeld G (ed) Distributed Computing, Lecture Notes in Computer Science, Springer Berlin Heidelberg, 5218,466\u2013480.\u00a0https:\/\/doi.org\/10.1007\/978-3-540-87779-0-32","DOI":"10.1007\/978-3-540-87779-0-32"}],"container-title":["Software Quality Journal"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11219-020-09539-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11219-020-09539-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11219-020-09539-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,9,1]],"date-time":"2021-09-01T10:18:03Z","timestamp":1630491483000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11219-020-09539-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,2,24]]},"references-count":37,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2021,9]]}},"alternative-id":["9539"],"URL":"https:\/\/doi.org\/10.1007\/s11219-020-09539-6","relation":{},"ISSN":["0963-9314","1573-1367"],"issn-type":[{"value":"0963-9314","type":"print"},{"value":"1573-1367","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,2,24]]},"assertion":[{"value":"9 November 2020","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"24 February 2021","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}