{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,11]],"date-time":"2025-09-11T11:30:43Z","timestamp":1757590243147,"version":"3.41.0"},"publisher-location":"Cham","reference-count":43,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319216898"},{"type":"electronic","value":"9783319216904"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","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":[[2015]]},"DOI":"10.1007\/978-3-319-21690-4_6","type":"book-chapter","created":{"date-parts":[[2015,7,15]],"date-time":"2015-07-15T06:08:27Z","timestamp":1436940507000},"page":"85-102","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":26,"title":["SMT and POR Beat Counter Abstraction: Parameterized Model Checking of\u00a0Threshold-Based Distributed Algorithms"],"prefix":"10.1007","author":[{"given":"Igor","family":"Konnov","sequence":"first","affiliation":[]},{"given":"Helmut","family":"Veith","sequence":"additional","affiliation":[]},{"given":"Josef","family":"Widder","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,7,16]]},"reference":[{"key":"6_CR1","unstructured":"https:\/\/github.com\/konnov\/fault-tolerant-benchmarks\/tree\/master\/2015"},{"key":"6_CR2","unstructured":"ByMC: Byzantine model checker. http:\/\/forsyte.tuwien.ac.at\/software\/bymc\/ (2013). Accessed Feb 2015"},{"issue":"5","key":"6_CR3","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1007\/s10009-008-0064-3","volume":"10","author":"S Bardin","year":"2008","unstructured":"Bardin, S., Finkel, A., Leroux, J., Petrucci, L.: Fast: acceleration from theory to practice. STTT 10(5), 401\u2013424 (2008)","journal-title":"STTT"},{"key":"6_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1007\/11817963_9","volume-title":"Computer Aided Verification","author":"S Bardin","year":"2006","unstructured":"Bardin, S., Leroux, J., Point, G.: FAST extended release. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 63\u201366. Springer, Heidelberg (2006)"},{"key":"6_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1007\/978-3-642-02658-4_9","volume-title":"Computer Aided Verification","author":"G Basler","year":"2009","unstructured":"Basler, G., Mazzucchi, M., Wahl, T., Kroening, D.: Symbolic counter abstraction for concurrent software. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 64\u201378. Springer, Heidelberg (2009)"},{"key":"6_CR6","unstructured":"Biere, A.: Lingeling, plingeling and treengeling entering the SAT competition 2013. In: Proceedings of SAT Competition 2013, Solver and p. 51 (2013)"},{"key":"6_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"A Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193\u2013207. Springer, Heidelberg (1999)"},{"key":"6_CR8","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":"6_CR9","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 32(4), 824\u2013840 (1985)","journal-title":"J. ACM"},{"key":"6_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1007\/3-540-44743-1_4","volume-title":"Parallel Computing Technologies","author":"F Brasileiro","year":"2001","unstructured":"Brasileiro, F., Greve, F.G.P., Most\u00e9faoui, A., Raynal, M.: Consensus in one communication step. In: Malyshkin, V.E. (ed.) PaCT 2001. LNCS, vol. 2127, pp. 42\u201350. Springer, Heidelberg (2001)"},{"key":"6_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"334","DOI":"10.1007\/978-3-319-08867-9_22","volume-title":"Computer Aided Verification","author":"R Cavada","year":"2014","unstructured":"Cavada, R., Cimatti, A., Dorigatti, M., Griggio, A., Mariotti, A., Micheli, A., Mover, S., Roveri, M., Tonetta, S.: The nuXmv symbolic model checker. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 334\u2013342. Springer, Heidelberg (2014)"},{"issue":"2","key":"6_CR12","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1145\/226643.226647","volume":"43","author":"TD Chandra","year":"1996","unstructured":"Chandra, T.D., Toueg, S.: Unreliable failure detectors for reliable distributed systems. JACM 43(2), 225\u2013267 (1996)","journal-title":"JACM"},{"issue":"5","key":"6_CR13","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 50(5), 752\u2013794 (2003)","journal-title":"J. ACM"},{"key":"6_CR14","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. 4963, pp. 33\u201347. Springer, Heidelberg (2008)"},{"key":"6_CR15","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. 3170, pp. 276\u2013291. Springer, Heidelberg (2004)"},{"key":"6_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/978-3-540-24622-0_9","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"E Clarke","year":"2004","unstructured":"Clarke, E., Kroning, D., Ouaknine, J., Strichman, O.: Completeness and complexity of bounded model checking. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 85\u201396. Springer, Heidelberg (2004)"},{"key":"6_CR17","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. 4963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"6_CR18","doi-asserted-by":"crossref","unstructured":"Dobre, D., Suri, N.: One-step consensus with zero-degradation. In: DSN, pp. 137\u2013146 (2006)","DOI":"10.1109\/DSN.2006.55"},{"key":"6_CR19","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Kahlon, V.: Model checking guarded protocols. In: LICS, pp. 361\u2013370, IEEE (2003)","DOI":"10.1109\/LICS.2003.1210076"},{"key":"6_CR20","doi-asserted-by":"crossref","unstructured":"Emerson, E., Namjoshi, K.: Reasoning about rings. In: POPL, pp. 85\u201394 (1995)","DOI":"10.1145\/199448.199468"},{"key":"6_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1007\/978-3-642-39799-8_8","volume-title":"Computer Aided Verification","author":"J Esparza","year":"2013","unstructured":"Esparza, J., Ganty, P., Majumdar, R.: Parameterized verification of asynchronous shared-memory systems. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 124\u2013140. Springer, Heidelberg (2013)"},{"key":"6_CR22","first-page":"176","volume-title":"CAV","author":"P Godefroid","year":"1990","unstructured":"Godefroid, P.: Using partial orders to improve automatic verifcation methods. In: Clarke, E.M., Kurshan, R.P. (eds.) CAV. LNCS, vol. 531, pp. 176\u2013185. Springer, Heidelberg (1990)"},{"issue":"1","key":"6_CR23","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/s446-002-8027-4","volume":"15","author":"R Guerraoui","year":"2002","unstructured":"Guerraoui, R.: Non-blocking atomic commit in asynchronous distributed systems with failure detectors. Distrib. Comput. 15(1), 17\u201325 (2002)","journal-title":"Distrib. Comput."},{"key":"6_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1007\/BFb0054186","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"HE Jensen","year":"1998","unstructured":"Jensen, H.E., Lynch, N.A.: A proof of burns n-process mutual exclusion algorithm using abstraction. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, p. 409. Springer, Heidelberg (1998)"},{"key":"6_CR25","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":"6_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"500","DOI":"10.1007\/978-3-642-32940-1_35","volume-title":"CONCUR 2012 \u2013 Concurrency Theory","author":"A Kaiser","year":"2012","unstructured":"Kaiser, A., Kroening, D., Wahl, T.: Efficient coverability analysis by proof minimization. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol. 7454, pp. 500\u2013515. Springer, Heidelberg (2012)"},{"key":"6_CR27","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 2, 328\u2013342 (2000)","journal-title":"STTT"},{"key":"6_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1007\/978-3-662-44584-6_10","volume-title":"CONCUR 2014 \u2013 Concurrency Theory","author":"I Konnov","year":"2014","unstructured":"Konnov, I., Veith, H., Widder, J.: On the completeness of bounded model checking for threshold-based distributed\u00a0algorithms: reachability. In: Baldan, P., Gorla, D. (eds.) CONCUR 2014. LNCS, vol. 8704, pp. 125\u2013140. Springer, Heidelberg (2014)"},{"key":"6_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/3-540-36384-X_24","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"D Kroning","year":"2002","unstructured":"Kroning, D., Strichman, O.: Efficient computation of recurrence diameters. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) VMCAI 2003. LNCS, vol. 2575, pp. 298\u2013309. Springer, Heidelberg (2002)"},{"issue":"7","key":"6_CR30","doi-asserted-by":"publisher","first-page":"558","DOI":"10.1145\/359545.359563","volume":"21","author":"L Lamport","year":"1978","unstructured":"Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Commun. ACM 21(7), 558\u2013565 (1978)","journal-title":"Commun. ACM"},{"key":"6_CR31","volume-title":"Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers","author":"L Lamport","year":"2002","unstructured":"Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley Longman Publishing Co., Inc., Boston (2002)"},{"key":"6_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"402","DOI":"10.1007\/978-3-540-28644-8_26","volume-title":"CONCUR 2004 - Concurrency Theory","author":"J Leroux","year":"2004","unstructured":"Leroux, J., Sutre, G.: On flatness for 2-dimensional vector addition systems with states. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 402\u2013416. Springer, Heidelberg (2004)"},{"key":"6_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"489","DOI":"10.1007\/11562948_36","volume-title":"Automated Technology for Verification and Analysis","author":"J Leroux","year":"2005","unstructured":"Leroux, J., Sutre, G.: Flat counter automata almost everywhere!. In: Peled, D.A., Tsay, Y.-K. (eds.) ATVA 2005. LNCS, vol. 3707, pp. 489\u2013503. Springer, Heidelberg (2005)"},{"issue":"12","key":"6_CR34","doi-asserted-by":"publisher","first-page":"717","DOI":"10.1145\/361227.361234","volume":"18","author":"RJ Lipton","year":"1975","unstructured":"Lipton, R.J.: Reduction: a method of proving properties of parallel programs. Commun. ACM 18(12), 717\u2013721 (1975)","journal-title":"Commun. ACM"},{"issue":"2","key":"6_CR35","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/BF00289237","volume":"21","author":"BD Lubachevsky","year":"1984","unstructured":"Lubachevsky, B.D.: An approach to automating the verification of compact parallel coordination programs. I. Acta Informatica 21(2), 125\u2013169 (1984)","journal-title":"I. Acta Informatica"},{"key":"6_CR36","volume-title":"Distributed Algorithms","author":"N Lynch","year":"1996","unstructured":"Lynch, N.: Distributed Algorithms. Morgan Kaufman, San Francisco (1996)"},{"key":"6_CR37","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":"6_CR38","first-page":"409","volume":"697","author":"D Peled","year":"1993","unstructured":"Peled, D.: All from one, one for all: on model checking using representatives. CAV. LNCS 697, 409\u2013423 (1993)","journal-title":"CAV. LNCS"},{"key":"6_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","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,\\infty )}$$ -counter abstraction. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 93\u2013111. Springer, Heidelberg (2002)"},{"key":"6_CR40","doi-asserted-by":"crossref","unstructured":"Raynal, M.: A case study of agreement problems in distributed systems: non-blocking atomic commitment. In: HASE, pp. 209\u2013214 (1997)","DOI":"10.1109\/HASE.1997.648067"},{"key":"6_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"438","DOI":"10.1007\/978-3-540-87779-0_30","volume-title":"Distributed Computing","author":"YJ Song","year":"2008","unstructured":"Song, Y.J., Van Renesse, R.: Bosco: one-step byzantine asynchronous consensus. In: Taubenfeld, G. (ed.) DISC 2008. LNCS, vol. 5218, pp. 438\u2013450. Springer, Heidelberg (2008)"},{"key":"6_CR42","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1007\/BF01667080","volume":"2","author":"T Srikanth","year":"1987","unstructured":"Srikanth, T., Toueg, S.: Simulating authenticated broadcasts to derive simple fault-tolerant algorithms. Dist. Comp. 2, 80\u201394 (1987)","journal-title":"Dist. Comp."},{"key":"6_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1007\/3-540-53863-1_36","volume-title":"Advances in Petri Nets 1990","author":"A Valmari","year":"1991","unstructured":"Valmari, A.: Stubborn sets for reduced state space generation. In: Rozenberg, G. (ed.) Advances in Petri Nets 1990. LNCS, vol. 483, pp. 491\u2013515. Springer, Heidelberg (1991)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-21690-4_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,29]],"date-time":"2025-05-29T06:28:19Z","timestamp":1748500099000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-21690-4_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319216898","9783319216904"],"references-count":43,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-21690-4_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"16 July 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}