{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,4]],"date-time":"2025-05-04T04:01:49Z","timestamp":1746331309980,"version":"3.40.4"},"publisher-location":"Cham","reference-count":81,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319073163"},{"type":"electronic","value":"9783319073170"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-07317-0_4","type":"book-chapter","created":{"date-parts":[[2014,5,26]],"date-time":"2014-05-26T01:53:38Z","timestamp":1401069218000},"page":"122-171","source":"Crossref","is-referenced-by-count":12,"title":["Tutorial on Parameterized Model Checking of Fault-Tolerant Distributed Algorithms"],"prefix":"10.1007","author":[{"given":"Annu","family":"Gmeiner","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Igor","family":"Konnov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ulrich","family":"Schmid","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Helmut","family":"Veith","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Josef","family":"Widder","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"4_CR1","unstructured":"ByMC 0.4.0: Byzantine model checker (2013), http:\/\/forsyte.tuwien.ac.at\/software\/bymc\/ (accessed March 2014)"},{"key":"4_CR2","unstructured":"Spin 6.2.7 (2014), http:\/\/spinroot.com\/ (accessed March 2014)"},{"key":"4_CR3","unstructured":"Tempo toolset. Web page, http:\/\/www.veromodo.com\/"},{"key":"4_CR4","unstructured":"TLA \u2013 the temporal logic of actions. Web page, http:\/\/research.microsoft.com\/en-us\/um\/people\/lamport\/tla\/tla.html"},{"key":"4_CR5","unstructured":"Yices 1.0.40 (2013), http:\/\/yices.csl.sri.com\/yices1-documentation.shtml (accessed March 2014)"},{"key":"4_CR6","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/s10009-011-0216-8","volume":"14","author":"P.A. Abdulla","year":"2012","unstructured":"Abdulla, P.A.: Regular model checking. International Journal on Software Tools for Technology Transfer\u00a014, 109\u2013118 (2012)","journal-title":"International Journal on Software Tools for Technology Transfer"},{"issue":"2","key":"4_CR7","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1006\/inco.1996.0053","volume":"127","author":"P.A. Abdulla","year":"1996","unstructured":"Abdulla, P.A., Jonsson, B.: Verifying programs with unreliable channels. Inf. Comput.\u00a0127(2), 91\u2013101 (1996)","journal-title":"Inf. Comput."},{"key":"4_CR8","doi-asserted-by":"crossref","unstructured":"Aguilera, M.K., Delporte-Gallet, C., Fauconnier, H., Toueg, S.: Consensus with Byzantine failures and little system synchrony. In: DSN, pp. 147\u2013155 (2006)","DOI":"10.1109\/DSN.2006.22"},{"issue":"1\/2","key":"4_CR9","first-page":"29","volume":"8","author":"F. Alberti","year":"2012","unstructured":"Alberti, F., Ghilardi, S., Pagani, E., Ranise, S., Rossi, G.P.: Universal guards, relativization of quantifiers, and failure models in model checking modulo theories. JSAT\u00a08(1\/2), 29\u201361 (2012)","journal-title":"JSAT"},{"key":"4_CR10","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1016\/0020-0190(86)90071-2","volume":"15","author":"K. Apt","year":"1986","unstructured":"Apt, K., Kozen, D.: Limits for automatic verification of finite-state concurrent systems. Inf. Process. Lett.\u00a015, 307\u2013309 (1986)","journal-title":"Inf. Process. Lett."},{"key":"4_CR11","doi-asserted-by":"crossref","unstructured":"Attiya, H., Welch, J.: Distributed Computing, 2nd edn. John Wiley & Sons (2004)","DOI":"10.1002\/0471478210"},{"key":"4_CR12","unstructured":"Baier, C., Katoen, J.P., Larsen, K.G.: Principles of Model Checking. MIT Press (2008)"},{"key":"4_CR13","doi-asserted-by":"crossref","unstructured":"Ball, T., Majumdar, R., Millstein, T.D., Rajamani, S.K.: Automatic predicate abstraction of c programs. In: PLDI, pp. 203\u2013213 (2001)","DOI":"10.1145\/381694.378846"},{"key":"4_CR14","unstructured":"Behrmann, G., David, A., Larsen, K.G.: A tutorial on uppaal 4.0 (2006)"},{"key":"4_CR15","doi-asserted-by":"crossref","unstructured":"Biely, M., Charron-Bost, B., Gaillard, A., Hutle, M., Schiper, A., Widder, J.: Tolerating corrupted communication. In: PODC, pp. 244\u2013253 (August 2007)","DOI":"10.1145\/1281100.1281136"},{"issue":"40","key":"4_CR16","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. Theoretical Computer Science\u00a0412(40), 5602\u20135630 (2011)","journal-title":"Theoretical Computer Science"},{"key":"4_CR17","unstructured":"Biere, A.: Handbook of satisfiability, vol.\u00a0185. IOS Press (2009)"},{"key":"4_CR18","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Fujita, M., Zhu, Y.: Symbolic model checking using SAT procedures instead of BDDs. In: DAC, pp. 317\u2013320 (1999)","DOI":"10.21236\/ADA360973"},{"key":"4_CR19","doi-asserted-by":"crossref","unstructured":"Bokor, P., Kinder, J., Serafini, M., Suri, N.: Efficient model checking of fault-tolerant distributed protocols. In: DSN, pp. 73\u201384 (2011)","DOI":"10.1109\/DSN.2011.5958208"},{"issue":"4","key":"4_CR20","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\u00a032(4), 824\u2013840 (1985)","journal-title":"J. ACM"},{"key":"4_CR21","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1016\/0890-5401(89)90026-6","volume":"81","author":"M.C. Browne","year":"1989","unstructured":"Browne, M.C., Clarke, E.M., Grumberg, O.: Reasoning about networks with many identical finite state processes. Inf. Comput.\u00a081, 13\u201331 (1989)","journal-title":"Inf. Comput."},{"key":"4_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"340","DOI":"10.1007\/978-3-540-85361-9_28","volume-title":"CONCUR 2008 - Concurrency Theory","author":"P. Chambart","year":"2008","unstructured":"Chambart, P., Schnoebelen, P.: Mixing lossy and perfect fifo channels. In: van Breugel, F., Chechik, M. (eds.) CONCUR 2008. LNCS, vol.\u00a05201, pp. 340\u2013355. Springer, Heidelberg (2008)"},{"issue":"2","key":"4_CR23","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1145\/226643.226647","volume":"43","author":"T.D. Chandra","year":"1996","unstructured":"Chandra, T.D., Toueg, S.: Unreliable failure detectors for reliable distributed systems. J. ACM\u00a043(2), 225\u2013267 (1996)","journal-title":"J. ACM"},{"key":"4_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1007\/978-3-642-24550-3_11","volume-title":"Stabilization, Safety, and Security of Distributed Systems","author":"B. Charron-Bost","year":"2011","unstructured":"Charron-Bost, B., Debrat, H., Merz, S.: Formal verification of consensus algorithms tolerating malicious faults. In: D\u00e9fago, X., Petit, F., Villain, V. (eds.) SSS 2011. LNCS, vol.\u00a06976, pp. 120\u2013134. Springer, Heidelberg (2011)"},{"key":"4_CR25","series-title":"LNCS","volume-title":"Replication: Theory and Practice","year":"2010","unstructured":"Charron-Bost, B., Pedone, F., Schiper, A. (eds.): Replication: Theory and Practice. LNCS, vol.\u00a05959. Springer, Heidelberg (2010)"},{"key":"4_CR26","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., Park, S.: A simple method for parameterized verification of cache coherence protocols. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol.\u00a03312, pp. 382\u2013398. Springer, Heidelberg (2004)"},{"issue":"5","key":"4_CR27","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"E. Clarke","year":"2003","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM\u00a050(5), 752\u2013794 (2003)","journal-title":"J. ACM"},{"key":"4_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/978-3-540-78800-3_4","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E. Clarke","year":"2008","unstructured":"Clarke, E., Talupur, M., Veith, H.: Proving Ptolemy right: the environment abstraction framework for model checking concurrent systems. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 33\u201347. Springer, Heidelberg (2008)"},{"key":"4_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"276","DOI":"10.1007\/978-3-540-28644-8_18","volume-title":"CONCUR 2004 - Concurrency Theory","author":"E. Clarke","year":"2004","unstructured":"Clarke, E., Talupur, M., Touili, T., Veith, H.: Verification by network decomposition. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol.\u00a03170, pp. 276\u2013291. Springer, Heidelberg (2004)"},{"key":"4_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Logics of Programs","author":"E.M. Clarke","year":"1982","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol.\u00a0131, pp. 52\u201371. Springer, Heidelberg (1982)"},{"key":"4_CR31","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press (1999)"},{"key":"4_CR32","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":"2006","unstructured":"Clarke, E., Talupur, M., Veith, H.: Environment abstraction for parameterized verification. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol.\u00a03855, pp. 126\u2013141. Springer, Heidelberg (2006)"},{"key":"4_CR33","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL, pp. 238\u2013252. ACM (1977)","DOI":"10.1145\/512950.512973"},{"issue":"4","key":"4_CR34","doi-asserted-by":"publisher","first-page":"451","DOI":"10.1145\/115372.115320","volume":"13","author":"R. Cytron","year":"1991","unstructured":"Cytron, R., Ferrante, J., Rosen, B.K., Wegman, M.N., Zadeck, F.K.: Efficiently computing static single assignment form and the control dependence graph. ACM Trans. Program. Lang. Syst.\u00a013(4), 451\u2013490 (1991)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"4_CR35","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. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.S.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"issue":"1","key":"4_CR36","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1109\/71.899936","volume":"12","author":"R. Prisco De","year":"2001","unstructured":"De Prisco, R., Malkhi, D., Reiter, M.K.: On k-set consensus problems in asynchronous systems. IEEE Trans. Parallel Distrib. Syst.\u00a012(1), 7\u201321 (2001)","journal-title":"IEEE Trans. Parallel Distrib. Syst."},{"issue":"3","key":"4_CR37","doi-asserted-by":"publisher","first-page":"499","DOI":"10.1145\/5925.5931","volume":"33","author":"D. Dolev","year":"1986","unstructured":"Dolev, D., Lynch, N.A., Pinter, S.S., Stark, E.W., Weihl, W.E.: Reaching approximate agreement in the presence of faults. J. ACM\u00a033(3), 499\u2013516 (1986)","journal-title":"J. ACM"},{"key":"4_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/11817963_11","volume-title":"Computer Aided Verification","author":"B. Dutertre","year":"2006","unstructured":"Dutertre, B., de Moura, L.: A fast linear-arithmetic solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 81\u201394. Springer, Heidelberg (2006)"},{"issue":"2","key":"4_CR39","doi-asserted-by":"publisher","first-page":"288","DOI":"10.1145\/42282.42283","volume":"35","author":"C. Dwork","year":"1988","unstructured":"Dwork, C., Lynch, N., Stockmeyer, L.: Consensus in the presence of partial synchrony. J. ACM\u00a035(2), 288\u2013323 (1988)","journal-title":"J. ACM"},{"key":"4_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1007\/10721959_19","volume-title":"Automated Deduction - CADE-17","author":"E.A. 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, vol.\u00a01831, pp. 236\u2013254. Springer, Heidelberg (2000)"},{"key":"4_CR41","doi-asserted-by":"crossref","unstructured":"Emerson, E., Namjoshi, K.: Reasoning about rings. In: POPL, pp. 85\u201394 (1995)","DOI":"10.1145\/199448.199468"},{"issue":"2","key":"4_CR42","doi-asserted-by":"publisher","first-page":"374","DOI":"10.1145\/3149.214121","volume":"32","author":"M.J. Fischer","year":"1985","unstructured":"Fischer, M.J., Lynch, N.A., Paterson, M.S.: Impossibility of distributed consensus with one faulty process. J. ACM\u00a032(2), 374\u2013382 (1985)","journal-title":"J. ACM"},{"key":"4_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1007\/978-3-540-78800-3_22","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D. Fisman","year":"2008","unstructured":"Fisman, D., Kupferman, O., Lustig, Y.: On verifying fault tolerance of distributed protocols. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 315\u2013331. Springer, Heidelberg (2008)"},{"key":"4_CR44","doi-asserted-by":"crossref","unstructured":"Fuegger, M., Schmid, U., Fuchs, G., Kempf, G.: Fault-Tolerant Distributed Clock Generation in VLSI Systems-on-Chip. In: EDCC 2006, pp. 87\u201396 (October 2006)","DOI":"10.1109\/EDCC.2006.11"},{"key":"4_CR45","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1145\/146637.146681","volume":"39","author":"S.M. German","year":"1992","unstructured":"German, S.M., Sistla, A.P.: Reasoning about systems with many processes. J. ACM\u00a039, 675\u2013735 (1992)","journal-title":"J. ACM"},{"key":"4_CR46","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., Sa\u00efdi, H.: Construction of abstract state graphs with pvs. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 72\u201383. Springer, Heidelberg (1997)"},{"key":"4_CR47","series-title":"Lecture Notes in Computer Science","volume-title":"25 Years of Model Checking","year":"2008","unstructured":"Grumberg, O., Veith, H. (eds.): 25 Years of Model Checking. LNCS, vol.\u00a05000. Springer, Heidelberg (2008)"},{"key":"4_CR48","doi-asserted-by":"publisher","first-page":"785","DOI":"10.1109\/32.159839","volume":"18","author":"N. Halbwachs","year":"1992","unstructured":"Halbwachs, N., Lagnier, F., Ratel, C.: Programming and verifying real-time systems by means of the synchronous data-flow language lustre. IEEE Trans. Softw. Eng.\u00a018, 785\u2013793 (1992)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"4_CR49","unstructured":"Holzmann, G.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley Professional (2003)"},{"key":"4_CR50","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/3-540-61474-5_65","volume-title":"Computer Aided Verification","author":"C. Ip","year":"1996","unstructured":"Ip, C., Dill, D.: Verifying systems with replicated components in mur\u03c6. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 147\u2013158. Springer, Heidelberg (1996)"},{"key":"4_CR51","doi-asserted-by":"crossref","unstructured":"John, A., Konnov, I., Schmid, U., Veith, H., Widder, J.: Starting a dialog between model checking and fault-tolerant distributed algorithms. arXiv CoRR abs\/1210.3839 (2012)","DOI":"10.1109\/FMCAD.2013.6679411"},{"key":"4_CR52","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: FMCAD, pp. 201\u2013209 (2013)","DOI":"10.1007\/978-3-642-39176-7_14"},{"key":"4_CR53","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.\u00a07976, pp. 209\u2013226. Springer, Heidelberg (2013)"},{"issue":"2","key":"4_CR54","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1023\/A:1022969405325","volume":"22","author":"R. Joshi","year":"2003","unstructured":"Joshi, R., Lamport, L., Matthews, J., Tasiran, S., Tuttle, M.R., Yu, Y.: Checking cache-coherence protocols with TLA\u2009+\u2009. Formal Methods in System Design\u00a022(2), 125\u2013131 (2003)","journal-title":"Formal Methods in System Design"},{"key":"4_CR55","doi-asserted-by":"crossref","unstructured":"Kaynar, D.K., Lynch, N.A., Segala, R., Vaandrager, F.W.: The Theory of Timed I\/O Automata. Synthesis Lectures on Computer Science. Morgan & Claypool (2006)","DOI":"10.2200\/S00006ED1V01Y200508CSL001"},{"key":"4_CR56","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/s100090050040","volume":"2","author":"Y. Kesten","year":"2000","unstructured":"Kesten, Y., Pnueli, A.: Control and data abstraction: the cornerstones of practical formal verification. STTT\u00a02, 328\u2013342 (2000)","journal-title":"STTT"},{"key":"4_CR57","unstructured":"Konnov, I., Veith, H., Widder, J.: Who is afraid of Model Checking Distributed Algorithms? (2012)"},{"key":"4_CR58","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1145\/279227.279229","volume":"16","author":"L. Lamport","year":"1998","unstructured":"Lamport, L.: The part-time parliament. ACM Trans. Comput. Syst.\u00a016, 133\u2013169 (1998)","journal-title":"ACM Trans. Comput. Syst."},{"key":"4_CR59","unstructured":"Lamport, L.: Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley (2002)"},{"key":"4_CR60","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/978-3-642-03466-4_2","volume-title":"Theoretical Aspects of Computing - ICTAC 2009","author":"L. Lamport","year":"2009","unstructured":"Lamport, L.: The pluscal algorithm language. In: Leucker, M., Morgan, C. (eds.) ICTAC 2009. LNCS, vol.\u00a05684, pp. 36\u201360. Springer, Heidelberg (2009)"},{"key":"4_CR61","doi-asserted-by":"crossref","unstructured":"Lincoln, P., Rushby, J.: A formally verified algorithm for interactive consistency under a hybrid fault model. In: FTCS-23, pp. 402\u2013411 (June 1993)","DOI":"10.1007\/3-540-56922-7_24"},{"key":"4_CR62","unstructured":"Lynch, N.: Distributed Algorithms. Morgan Kaufman, San Francisco (1996)"},{"key":"4_CR63","unstructured":"Lynch, N., Tuttle, M.: An introduction to input\/output automata. Tech. Rep. MIT\/LCS\/TM-373, Laboratory for Computer Science, MIT (1989)"},{"key":"4_CR64","doi-asserted-by":"crossref","unstructured":"McMillan, K.: Symbolic model checking. Kluwer (1993)","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"4_CR65","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":"K.L. McMillan","year":"2001","unstructured":"McMillan, K.L.: Parameterized verification of the flash cache coherence protocol by compositional model checking. In: Margaria, T., Melham, T.F. (eds.) CHARME 2001. LNCS, vol.\u00a02144, pp. 179\u2013195. Springer, Heidelberg (2001)"},{"issue":"8","key":"4_CR66","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1016\/j.entcs.2006.11.040","volume":"174","author":"S. Mitra","year":"2007","unstructured":"Mitra, S., Lynch, N.A.: Proving approximate implementations for probabilistic I\/O automata. Electr. Notes Theor. Comput. Sci.\u00a0174(8), 71\u201393 (2007)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"4_CR67","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: DSN, pp. 541\u2013550 (2003)","DOI":"10.1109\/DSN.2003.1209964"},{"key":"4_CR68","doi-asserted-by":"crossref","unstructured":"O\u2019Leary, J.W., Talupur, M., Tuttle, M.R.: Protocol verification using flows: An industrial experience. In: FMCAD, pp. 172\u2013179 (2009)","DOI":"10.1109\/FMCAD.2009.5351126"},{"issue":"2","key":"4_CR69","doi-asserted-by":"publisher","first-page":"228","DOI":"10.1145\/322186.322188","volume":"27","author":"M. Pease","year":"1980","unstructured":"Pease, M., Shostak, R., Lamport, L.: Reaching agreement in the presence of faults. J. ACM\u00a027(2), 228\u2013234 (1980)","journal-title":"J. ACM"},{"key":"4_CR70","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/3-540-45657-0_9","volume-title":"Computer Aided Verification","author":"A. Pnueli","year":"2002","unstructured":"Pnueli, A., Xu, J., Zuck, L.D.: Liveness with (0,1,\u2009\u221e\u2009)-counter abstraction. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 107\u2013111. Springer, Heidelberg (2002)"},{"key":"4_CR71","doi-asserted-by":"crossref","unstructured":"Powell, D.: Failure mode assumptions and assumption coverage. In: FTCS-22, Boston, MA, USA, pp. 386\u2013395 (1992)","DOI":"10.1109\/FTCS.1992.243562"},{"key":"4_CR72","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"304","DOI":"10.1007\/BFb0028994","volume-title":"STACS 89","author":"N. Santoro","year":"1989","unstructured":"Santoro, N., Widmayer, P.: Time is not a healer. In: Cori, R., Monien, B. (eds.) STACS 1989. LNCS, vol.\u00a0349, pp. 304\u2013313. Springer, Heidelberg (1989)"},{"key":"4_CR73","doi-asserted-by":"crossref","unstructured":"Schmid, U., Weiss, B., Rushby, J.: Formally verified Byzantine agreement in presence of link faults. In: ICDCS, July 2-5, pp. 608\u2013616 (2002)","DOI":"10.1109\/ICDCS.2002.1022311"},{"issue":"11","key":"4_CR74","doi-asserted-by":"publisher","first-page":"1313","DOI":"10.1016\/j.ic.2008.07.004","volume":"206","author":"S. Shoham","year":"2008","unstructured":"Shoham, S., Grumberg, O.: 3-valued abstraction: More precision at less cost. Inf. Comput.\u00a0206(11), 1313\u20131333 (2008)","journal-title":"Inf. Comput."},{"issue":"3","key":"4_CR75","doi-asserted-by":"publisher","first-page":"626","DOI":"10.1145\/28869.28876","volume":"34","author":"T.K. Srikanth","year":"1987","unstructured":"Srikanth, T.K., Toueg, S.: Optimal clock synchronization. Journal of the ACM\u00a034(3), 626\u2013645 (1987)","journal-title":"Journal of the ACM"},{"key":"4_CR76","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. Distributed Computing\u00a02, 80\u201394 (1987)","journal-title":"Distributed Computing"},{"issue":"4","key":"4_CR77","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.\u00a028(4), 213\u2013214 (1988)","journal-title":"Inf. Process. Lett."},{"issue":"5-6","key":"4_CR78","doi-asserted-by":"publisher","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\u00a023(5-6), 341\u2013358 (2011)","journal-title":"Distributed Computing"},{"issue":"6","key":"4_CR79","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/s00446-011-0147-3","volume":"24","author":"J. Widder","year":"2012","unstructured":"Widder, J., Biely, M., Gridling, G., Weiss, B., Blanquart, J.P.: Consensus in the presence of mortal Byzantine faulty processes. Distributed Computing\u00a024(6), 299\u2013321 (2012)","journal-title":"Distributed Computing"},{"issue":"2","key":"4_CR80","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/s00446-007-0026-0","volume":"20","author":"J. Widder","year":"2007","unstructured":"Widder, J., Schmid, U.: Booting clock synchronization in partially synchronous systems with hybrid process and link failures. Distributed Computing\u00a020(2), 115\u2013140 (2007)","journal-title":"Distributed Computing"},{"key":"4_CR81","doi-asserted-by":"crossref","unstructured":"W\u00f6hrle, S., Thomas, W.: Model checking synchronized products of infinite transition systems. LMCS\u00a03(4) (2007)","DOI":"10.2168\/LMCS-3(4:5)2007"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Executable Software Models"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-07317-0_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,3]],"date-time":"2025-05-03T03:13:12Z","timestamp":1746241992000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-07317-0_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319073163","9783319073170"],"references-count":81,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-07317-0_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}