{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:25:07Z","timestamp":1759638307285},"publisher-location":"Cham","reference-count":55,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319737201"},{"type":"electronic","value":"9783319737218"}],"license":[{"start":{"date-parts":[[2017,12,29]],"date-time":"2017-12-29T00:00:00Z","timestamp":1514505600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-73721-8_1","type":"book-chapter","created":{"date-parts":[[2017,12,28]],"date-time":"2017-12-28T09:13:05Z","timestamp":1514452385000},"page":"1-24","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["Parameterized Model Checking of Synchronous Distributed Algorithms by Abstraction"],"prefix":"10.1007","author":[{"given":"Benjamin","family":"Aminof","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sasha","family":"Rubin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ilina","family":"Stoilkovska","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Josef","family":"Widder","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Florian","family":"Zuleger","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,12,29]]},"reference":[{"key":"1_CR1","unstructured":"Aiswarya, C., Bollig, B., Gastin, P.: An automata-theoretic approach to the verification of distributed algorithms. In: 26th International Conference on Concurrency Theory, CONCUR 2015, Madrid, Spain, September 1.4, 2015, pp. 340\u2013353 (2015)"},{"key":"1_CR2","unstructured":"Alberti, F., Ghilardi, S., Orsini, A., Pagani, E.: Counter abstractions in model checking of distributed broadcast algorithms: some case studies. In: Proceedings of the 31st Italian Conference on Computational Logic, Milano, Italy, June 20\u201322, 2016, pp. 102\u2013117 (2016)"},{"key":"1_CR3","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"},{"issue":"6","key":"1_CR4","doi-asserted-by":"crossref","first-page":"307","DOI":"10.1016\/0020-0190(86)90071-2","volume":"22","author":"KR Apt","year":"1986","unstructured":"Apt, K.R., Kozen, D.: Limits for Automatic Verification of Finite-State Concurrent Systems. Inf. Process. Lett. 22(6), 307\u2013309 (1986)","journal-title":"Inf. Process. Lett."},{"key":"1_CR5","doi-asserted-by":"crossref","unstructured":"Attiya, H., Welch, J.: Distributed Computing, 2nd edn. Wiley (2004)","DOI":"10.1002\/0471478210"},{"key":"1_CR6","doi-asserted-by":"crossref","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 (2015)","DOI":"10.2200\/S00658ED1V01Y201508DCT013"},{"issue":"1","key":"1_CR7","doi-asserted-by":"crossref","first-page":"13","DOI":"10.1016\/0890-5401(89)90026-6","volume":"81","author":"MC Browne","year":"1989","unstructured":"Browne, M.C., Clarke, E.M., Grumberg, O.: Reasoning about Networks with Many Identical Finite State Processes. Inf. Comput. 81(1), 13\u201331 (1989)","journal-title":"Inf. Comput."},{"key":"1_CR8","unstructured":"Burrows, M.: The chubby lock service for loosely-coupled distributed systems. In: 7th Symposium on Operating Systems Design and Implementation (OSDI 2006), Seattle, WA, USA, November 6\u20138, pp. 335\u2013350 (2006)"},{"key":"1_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1007\/978-3-319-59647-1_16","volume-title":"Networked Systems","author":"A Casta\u00f1eda","year":"2017","unstructured":"Casta\u00f1eda, A., Moses, Y., Raynal, M., Roy, M.: Early decision and stopping in synchronous consensus: a predicate-based guided tour. In: El Abbadi, A., Garbinato, B. (eds.) NETYS 2017. LNCS, vol. 10299, pp. 206\u2013221. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-59647-1_16"},{"key":"1_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-642-04420-5_10","volume-title":"Reachability Problems","author":"M Chaouch-Saad","year":"2009","unstructured":"Chaouch-Saad, M., Charron-Bost, B., Merz, S.: A reduction theorem for the verification of round-based distributed algorithms. In: Bournez, O., Potapov, I. (eds.) RP 2009. LNCS, vol. 5797, pp. 93\u2013106. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-04420-5_10"},{"issue":"1","key":"1_CR11","doi-asserted-by":"crossref","first-page":"15","DOI":"10.1016\/j.jalgor.2003.11.001","volume":"51","author":"B Charron-Bost","year":"2004","unstructured":"Charron-Bost, B., Schiper, A.: Uniform Consensus is Harder than Consensus. J. Algorithms 51(1), 15\u201337 (2004)","journal-title":"J. Algorithms"},{"issue":"1","key":"1_CR12","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1007\/s00446-009-0084-6","volume":"22","author":"B Charron-Bost","year":"2009","unstructured":"Charron-Bost, B., Schiper, A.: The Heard-Of Model: Computing in Distributed Systems with Benign Faults. Distributed Computing 22(1), 49\u201371 (2009)","journal-title":"Distributed Computing"},{"key":"1_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"382","DOI":"10.1007\/978-3-540-30494-4_27","volume-title":"Formal Methods in Computer-Aided Design","author":"C-T Chou","year":"2004","unstructured":"Chou, C.-T., Mannava, P.K., Park, S.: A simple method for parameterized verification of cache coherence protocols. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol. 3312, pp. 382\u2013398. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-30494-4_27"},{"issue":"5","key":"1_CR14","doi-asserted-by":"crossref","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"EM Clarke","year":"1994","unstructured":"Clarke, E.M., Grumberg, O., Long, D.E.: Model Checking and Abstraction. ACM Trans. Program. Lang. Syst. 16(5), 1512\u20131542 (1994)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"1_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/11609773_9","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"E Clarke","year":"2005","unstructured":"Clarke, E., Talupur, M., Veith, H.: Environment abstraction for parameterized verification. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 126\u2013141. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11609773_9"},{"key":"1_CR16","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Talupur, M., Veith, H.: Proving ptolemy right: the environment abstraction framework for model checking concurrent systems. In: Proceedings of 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29\u2013April 6, 2008, pp. 33\u201347 (2008)","DOI":"10.1007\/978-3-540-78800-3_4"},{"key":"1_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/978-3-642-54013-4_10","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"C Dr\u0103goi","year":"2014","unstructured":"Dr\u0103goi, C., Henzinger, T.A., Veith, H., Widder, J., Zufferey, D.: A logic-based framework for verifying consensus algorithms. In: McMillan, K.L., Rival, X. (eds.) VMCAI 2014. LNCS, vol. 8318, pp. 161\u2013181. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54013-4_10"},{"key":"1_CR18","doi-asserted-by":"crossref","unstructured":"Dragoi, C., Henzinger, T.A., Zufferey, D.: PSync: a partially synchronous language for fault-tolerant distributed algorithms. In: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20\u201322, 2016, pp. 400\u2013415 (2016)","DOI":"10.1145\/2837614.2837650"},{"key":"1_CR19","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Namjoshi, K.S.: Reasoning about rings. In: Conference Record of POPL 1995: 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Francisco, California, USA, January 23\u201325, 1995, pp. 85\u201394 (1995)","DOI":"10.1145\/199448.199468"},{"issue":"1\/2","key":"1_CR20","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1007\/BF00625970","volume":"9","author":"EA Emerson","year":"1996","unstructured":"Emerson, E.A., Sistla, A.P.: Symmetry and Model Checking. Formal Methods in System Design 9(1\/2), 105\u2013131 (1996)","journal-title":"Formal Methods in System Design"},{"issue":"2","key":"1_CR21","doi-asserted-by":"crossref","first-page":"374","DOI":"10.1145\/3149.214121","volume":"32","author":"MJ Fischer","year":"1985","unstructured":"Fischer, M.J., Lynch, N.A., Paterson, M.: Impossibility of distributed consensus with one faulty process. J. ACM 32(2), 374\u2013382 (1985)","journal-title":"J. ACM"},{"key":"1_CR22","doi-asserted-by":"crossref","unstructured":"Fisman, D., Kupferman, O., Lustig, Y.: On verifying fault tolerance of distributed protocols. In: Proceedings of 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29\u2013April 6, 2008, pp. 315\u2013331 (2008)","DOI":"10.1007\/978-3-540-78800-3_22"},{"key":"1_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification","author":"S Graf","year":"1997","unstructured":"Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72\u201383. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/3-540-63166-6_10"},{"key":"1_CR24","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: Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, October 20\u201323, 2013, pp. 201\u2013209 (2013)","DOI":"10.1109\/FMCAD.2013.6679411"},{"key":"1_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/978-3-642-39176-7_14","volume-title":"Model Checking Software","author":"A John","year":"2013","unstructured":"John, A., Konnov, I., Schmid, U., Veith, H., Widder, J.: Towards modeling and model checking fault-tolerant distributed algorithms. In: Bartocci, E., Ramakrishnan, C.R. (eds.) SPIN 2013. LNCS, vol. 7976, pp. 209\u2013226. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39176-7_14"},{"key":"1_CR26","doi-asserted-by":"crossref","unstructured":"Killian, C.E., Anderson, J.W., Braud, R., Jhala, R., Vahdat, A.: Mace: language support for building distributed systems. In: Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, San Diego, California, USA, June 10\u201313, 2007, pp. 179\u2013188 (2007)","DOI":"10.1145\/1250734.1250755"},{"issue":"2","key":"1_CR27","doi-asserted-by":"crossref","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 Methods in System Design 51(2), 270\u2013307 (2017)","journal-title":"Formal Methods in System Design"},{"key":"1_CR28","doi-asserted-by":"crossref","unstructured":"Konnov, I.V., 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, POPL 2017, Paris, France, January 18\u201320, 2017, pp. 719\u2013734 (2017)","DOI":"10.1145\/3009837.3009860"},{"key":"1_CR29","doi-asserted-by":"crossref","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)","journal-title":"Inf. Comput."},{"issue":"1","key":"1_CR30","doi-asserted-by":"crossref","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":"4","key":"1_CR31","doi-asserted-by":"crossref","first-page":"7:1","DOI":"10.1145\/1658357.1658358","volume":"27","author":"R Kotla","year":"2009","unstructured":"Kotla, R., Alvisi, L., Dahlin, M., Clement, A., Wong, E.L.: Zyzzyva: Speculative Byzantine Fault Tolerance. ACM Trans. Comput. Syst. 27(4), 7:1\u20137:39 (2009)","journal-title":"ACM Trans. Comput. Syst."},{"key":"1_CR32","unstructured":"Krsti\u0107, S.: Parametrized system verification with guard strengthening and parameter abstraction. In: AVIS, 2005 (2005)"},{"key":"1_CR33","unstructured":"Lamport, L.: Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley (2002)"},{"issue":"3","key":"1_CR34","doi-asserted-by":"crossref","first-page":"382","DOI":"10.1145\/357172.357176","volume":"4","author":"L Lamport","year":"1982","unstructured":"Lamport, L., Shostak, R.E., Pease, M.C.: The Byzantine Generals Problem. ACM Trans. Program. Lang. Syst. 4(3), 382\u2013401 (1982)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"1_CR35","doi-asserted-by":"crossref","unstructured":"Lesani, M., Bell, C.J., Chlipala, A.: Chapar: certified causally consistent distributed key-value stores. In: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20\u201322, 2016, pp. 357\u2013370 (2016)","DOI":"10.1145\/2837614.2837622"},{"key":"1_CR36","doi-asserted-by":"crossref","unstructured":"Lincoln, P., Rushby, J.M.: A formally verified algorithm for interactive consistency under a hybrid fault model. In: Digest of Papers: FTCS-23, The Twenty-Third Annual International Symposium on Fault-Tolerant Computing, Toulouse, France, June 22\u201324, 1993, pp. 402\u2013411 (1993)","DOI":"10.1109\/FTCS.1993.627343"},{"key":"1_CR37","unstructured":"Lynch, N.A.: Distributed Algorithms. Morgan Kaufmann (1996)"},{"key":"1_CR38","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":"1_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/3-540-48153-2_17","volume-title":"Correct Hardware Design and Verification Methods","author":"KL McMillan","year":"1999","unstructured":"McMillan, K.L.: Verification of infinite state systems by compositional model checking. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 219\u2013237. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48153-2_17"},{"key":"1_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/3-540-44798-9_17","volume-title":"Correct Hardware Design and Verification Methods","author":"KL McMillan","year":"2001","unstructured":"McMillan, K.L.: Parameterized verification of the flash cache coherence protocol by compositional model checking. In: Margaria, T., Melham, T. (eds.) CHARME 2001. LNCS, vol. 2144, pp. 179\u2013195. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44798-9_17"},{"key":"1_CR41","unstructured":"Medeiros, A.: ZooKeeper\u2019s atomic broadcast protocol: Theory and practice. Technical report (2012)"},{"key":"1_CR42","doi-asserted-by":"crossref","unstructured":"Moraru, I., Andersen, D.G., Kaminsky, M.: There is more consensus in egalitarian parliaments. In: ACM SIGOPS 24th Symposium on Operating Systems Principles, SOSP 2013, Farmington, PA, USA, November 3\u20136, 2013, pp. 358\u2013372 (2013)","DOI":"10.1145\/2517349.2517350"},{"key":"1_CR43","doi-asserted-by":"crossref","unstructured":"O\u2019Leary, J.W., Talupur, M., Tuttle, M.R.: Protocol verification using flows: an industrial experience. In: Proceedings of 9th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2009, Austin, Texas, USA, November 15\u201318, 2009, pp. 172\u2013179 (2009)","DOI":"10.1109\/FMCAD.2009.5351126"},{"issue":"2","key":"1_CR44","doi-asserted-by":"crossref","first-page":"228","DOI":"10.1145\/322186.322188","volume":"27","author":"MC Pease","year":"1980","unstructured":"Pease, M.C., Shostak, R.E., Lamport, L.: Reaching Agreement in the Presence of Faults. J. ACM 27(2), 228\u2013234 (1980)","journal-title":"J. ACM"},{"key":"1_CR45","doi-asserted-by":"crossref","unstructured":"Peluso, S., Turcu, A., Palmieri, R., Losa, G., Ravindran, B.: Making fast consensus generally faster. In: 46th Annual IEEE\/IFIP International Conference on Dependable Systems and Networks, DSN 2016, Toulouse, France, June 28 \u2013July 1, 2016, pp. 156\u2013167 (2016)","DOI":"10.1109\/DSN.2016.23"},{"key":"1_CR46","unstructured":"Pnueli, A., Xu, J., Zuck, L.D.: Liveness with (0, 1, infty)-counter abstraction. In: Proceedings of 14th International Conference on Computer Aided Verification, CAV 2002, Copenhagen, Denmark, July 27\u201331, 2002, pp. 107\u2013122 (2002)"},{"key":"1_CR47","doi-asserted-by":"crossref","unstructured":"Raynal, M.: Fault-tolerant Agreement in Synchronous Message-passing Systems. Synthesis Lectures on Distributed Computing Theory. Morgan & Claypool Publishers (2010)","DOI":"10.2200\/S00294ED1V01Y201009DCT003"},{"key":"1_CR48","doi-asserted-by":"crossref","unstructured":"Steiner, W., Rushby, J.M., Sorea, M., Pfeifer, H.: Model checking a fault-tolerant startup algorithm: from design exploration to exhaustive fault simulation. In: Proceedings of 2004 International Conference on Dependable Systems and Networks (DSN 2004), Florence, Italy, 28 June - 1 July 2004, pp. 189\u2013198 (2004)","DOI":"10.1109\/DSN.2004.1311889"},{"issue":"4","key":"1_CR49","doi-asserted-by":"crossref","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)","journal-title":"Inf. Process. Lett."},{"key":"1_CR50","unstructured":"TLA+ Toolbox. http:\/\/research.microsoft.com\/en-us\/um\/people\/lamport\/tla\/tools.html"},{"issue":"5\u20136","key":"1_CR51","doi-asserted-by":"crossref","first-page":"341","DOI":"10.1007\/s00446-010-0123-3","volume":"23","author":"T Tsuchiya","year":"2011","unstructured":"Tsuchiya, T., Schiper, A.: Verification of consensus algorithms using satisfiability solving. Distributed Computing 23(5\u20136), 341\u2013358 (2011)","journal-title":"Distributed Computing"},{"key":"1_CR52","doi-asserted-by":"crossref","unstructured":"von Gleissenthall, K., Bj\u00f8rner, N., Rybalchenko, A.: Cardinalities and universal quantifiers for verifying parameterized systems. In: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016, Santa Barbara, CA, USA, June 13\u201317, 2016, pp. 599\u2013613 (2016)","DOI":"10.1145\/2908080.2908129"},{"key":"1_CR53","doi-asserted-by":"crossref","unstructured":"Widder, J., Gridling, G., Weiss, B., Blanquart, J.-P.: Synchronous consensus with Mortal Byzantines. In: Proceedings of The 37th Annual IEEE\/IFIP International Conference on Dependable Systems and Networks, DSN 2007, Edinburgh, UK, June 25\u201328, 2007, pp. 102\u2013112 (2007)","DOI":"10.1109\/DSN.2007.91"},{"key":"1_CR54","doi-asserted-by":"crossref","unstructured":"Woos, D., Wilcox, J.R., Anton, S., Tatlock, Z., Ernst, M.D., Anderson, T.E.: Planning for change in a formal verification of the RAFT consensus protocol. In: Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, Saint Petersburg, FL, USA, January 20\u201322, 2016, pp. 154\u2013165 (2016)","DOI":"10.1145\/2854065.2854081"},{"key":"1_CR55","unstructured":"ZooKeeper, A.: http:\/\/zookeeper.apache.org\/"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-73721-8_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,8]],"date-time":"2019-10-08T20:00:36Z","timestamp":1570564836000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-73721-8_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,12,29]]},"ISBN":["9783319737201","9783319737218"],"references-count":55,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-73721-8_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017,12,29]]}}}