{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T12:11:00Z","timestamp":1781007060241,"version":"3.54.1"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642540127","type":"print"},{"value":"9783642540134","type":"electronic"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"tdm","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-642-54013-4_10","type":"book-chapter","created":{"date-parts":[[2014,1,3]],"date-time":"2014-01-03T01:08:09Z","timestamp":1388711289000},"page":"161-181","source":"Crossref","is-referenced-by-count":38,"title":["A Logic-Based Framework for Verifying Consensus Algorithms"],"prefix":"10.1007","author":[{"given":"Cezara","family":"Dr\u0103goi","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Thomas A.","family":"Henzinger","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Helmut","family":"Veith","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Josef","family":"Widder","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Damien","family":"Zufferey","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"10_CR1","unstructured":"Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.K.: General decidability theorems for infinite-state systems (1996)"},{"key":"10_CR2","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":"10_CR3","doi-asserted-by":"crossref","unstructured":"Ben-Or, M.: Another advantage of free choice (extended abstract): Completely asynchronous agreement protocols. In: PODC, pp. 27\u201330. ACM (1983)","DOI":"10.1145\/800221.806707"},{"key":"10_CR4","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 (2007)","DOI":"10.1145\/1281100.1281136"},{"key":"10_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/978-3-642-04081-8_13","volume-title":"CONCUR 2009 - Concurrency Theory","author":"A. Bouajjani","year":"2009","unstructured":"Bouajjani, A., Dr\u0103goi, C., Enea, C., Sighireanu, M.: A logic-based framework for reasoning about composite data structures. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009. LNCS, vol.\u00a05710, pp. 178\u2013195. Springer, Heidelberg (2009)"},{"key":"10_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/11609773_28","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A.R. Bradley","year":"2006","unstructured":"Bradley, A.R., Manna, Z., Sipma, H.B.: What\u2019s decidable about arrays? In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol.\u00a03855, pp. 427\u2013442. Springer, Heidelberg (2006)"},{"key":"10_CR7","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.\u00a02127, pp. 42\u201350. Springer, Heidelberg (2001)"},{"key":"10_CR8","volume-title":"OSDI","author":"M. Burrows","year":"2006","unstructured":"Burrows, M.: The chubby lock service for loosely-coupled distributed systems. In: OSDI. USENIX Association, Berkeley (2006)"},{"issue":"2-3","key":"10_CR9","first-page":"273","volume":"3","author":"B. Charron-Bost","year":"2009","unstructured":"Charron-Bost, B., Merz, S.: Formal verification of a consensus algorithm in the heard-of model. Int. J. Software and Informatics\u00a03(2-3), 273\u2013303 (2009)","journal-title":"Int. J. Software and Informatics"},{"issue":"1","key":"10_CR10","doi-asserted-by":"publisher","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\u00a022(1), 49\u201371 (2009)","journal-title":"Distributed Computing"},{"issue":"2","key":"10_CR11","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"},{"issue":"6","key":"10_CR12","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1007\/s00446-011-0151-7","volume":"24","author":"M. F\u00fcgger","year":"2012","unstructured":"F\u00fcgger, M., Schmid, U.: Reconciling fault-tolerant distributed computing and systems-on-chip. Dist. Comp.\u00a024(6), 323\u2013355 (2012)","journal-title":"Dist. Comp."},{"key":"10_CR13","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. Journal of the ACM\u00a039, 675\u2013735 (1992)","journal-title":"Journal of the ACM"},{"key":"10_CR14","unstructured":"Hunt, P., Konar, M., Junqueira, F.P., Reed, B.: Zookeeper: wait-free coordination for internet-scale systems. In: USENIXATC. USENIX Association (2010)"},{"key":"10_CR15","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":"10_CR16","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/11532231_20","volume-title":"Automated Deduction \u2013 CADE-20","author":"V. Kuncak","year":"2005","unstructured":"Kuncak, V., Nguyen, H.H., Rinard, M.: An algorithm for deciding BAPA: Boolean algebra with presburger arithmetic. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol.\u00a03632, pp. 260\u2013277. Springer, Heidelberg (2005)"},{"key":"10_CR17","doi-asserted-by":"crossref","unstructured":"Lamport, L.: The part-time parliament. ACM Trans. Comput. Syst. (1998)","DOI":"10.1145\/279227.279229"},{"key":"10_CR18","doi-asserted-by":"crossref","unstructured":"Lamport, L.: Distributed algorithms in TLA (abstract). In: PODC (2000)","DOI":"10.1145\/343477.343497"},{"key":"10_CR19","unstructured":"Lynch, N.: Distributed Algorithms. Morgan Kaufman (1996)"},{"key":"10_CR20","doi-asserted-by":"crossref","unstructured":"Madhusudan, P., Parlato, G., Qiu, X.: Decidable logics combining heap structures and data. In: POPL, pp. 611\u2013622. ACM (2011)","DOI":"10.1145\/1925844.1926455"},{"key":"10_CR21","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.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"10_CR22","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)"},{"issue":"4","key":"10_CR23","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."},{"key":"10_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"380","DOI":"10.1007\/978-3-642-11319-2_27","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"K. Yessenov","year":"2010","unstructured":"Yessenov, K., Piskac, R., Kuncak, V.: Collections, cardinalities, and relations. In: Barthe, G., Hermenegildo, M. (eds.) VMCAI 2010. LNCS, vol.\u00a05944, pp. 380\u2013395. Springer, Heidelberg (2010)"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-54013-4_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,25]],"date-time":"2019-05-25T23:40:21Z","timestamp":1558827621000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-54013-4_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783642540127","9783642540134"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-54013-4_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]}}}