{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T04:57:18Z","timestamp":1725857838899},"publisher-location":"Cham","reference-count":23,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319402284"},{"type":"electronic","value":"9783319402291"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[[2016]]},"DOI":"10.1007\/978-3-319-40229-1_6","type":"book-chapter","created":{"date-parts":[[2016,6,11]],"date-time":"2016-06-11T08:54:04Z","timestamp":1465635244000},"page":"65-81","source":"Crossref","is-referenced-by-count":10,"title":["Counting Constraints in Flat Array Fragments"],"prefix":"10.1007","author":[{"given":"Francesco","family":"Alberti","sequence":"first","affiliation":[]},{"given":"Silvio","family":"Ghilardi","sequence":"additional","affiliation":[]},{"given":"Elena","family":"Pagani","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,6,12]]},"reference":[{"key":"6_CR1","unstructured":"Alberti, F., Ghilardi, S., Pagani, E.: Counting constraints in flat array fragments (2016). CoRR, abs\/1602.00458"},{"key":"6_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"15","DOI":"10.1007\/978-3-642-54862-8_2","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"F Alberti","year":"2014","unstructured":"Alberti, F., Ghilardi, S., Sharygina, N.: Decision procedures for flat array properties. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol. 8413, pp. 15\u201330. Springer, Heidelberg (2014)"},{"key":"6_CR3","doi-asserted-by":"crossref","unstructured":"Biely, M., Charron-Bost, B., Gaillard, A., Hutle, M., Schiper, A., Widder, J.: Tolerating corrupted communication. In: Proceedings of PODC, pp. 244\u2013253 (2007)","DOI":"10.1145\/1281100.1281136"},{"key":"6_CR4","unstructured":"Bj\u00f8rner, N., von Gleissenthall, K., Rybalchenko, A.: Synthesizing cardinality invariants for parameterized systems (2015). https:\/\/www7.in.tum.de\/~gleissen\/papers\/sharpie.pdf"},{"key":"6_CR5","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. Distrib. Comput. 22, 49\u201371 (2009)","journal-title":"Distrib. Comput."},{"key":"6_CR6","first-page":"43","volume-title":"Programming Languages","author":"EW Dijkstra","year":"1968","unstructured":"Dijkstra, E.W.: Cooperating sequential processes. In: Genuys, F. (ed.) Programming Languages, pp. 43\u2013112. Academic Press, New York (1968)"},{"key":"6_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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)"},{"key":"6_CR8","unstructured":"Dragoi, C., Henzinger, T.A., Zufferey, D.: The need for language support for fault-tolerant distributed systems. In: Proceedings of SNAPL (2015)"},{"issue":"5","key":"6_CR9","doi-asserted-by":"crossref","first-page":"564","DOI":"10.1016\/j.orl.2005.09.008","volume":"34","author":"F Eisenbrand","year":"2006","unstructured":"Eisenbrand, F., Shmonin, G.: Carath\u00e9odory bounds for integer cones. Oper. Res. Lett. 34(5), 564\u2013568 (2006)","journal-title":"Oper. Res. Lett."},{"issue":"2","key":"6_CR10","doi-asserted-by":"crossref","first-page":"637","DOI":"10.2307\/2274706","volume":"56","author":"JY Halpern","year":"1991","unstructured":"Halpern, J.Y.: Presburger arithmetic with unary predicates is $$\\Pi ^1_1$$ complete. J. Symbol. Logic 56(2), 637\u2013642 (1991)","journal-title":"J. Symbol. Logic"},{"key":"6_CR11","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: Proceedings of FMCAD, pp. 201\u2013209, August 2013","DOI":"10.1109\/FMCAD.2013.6679411"},{"key":"6_CR12","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_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1007\/978-3-319-21690-4_6","volume-title":"Computer Aided Verification","author":"I Konnov","year":"2015","unstructured":"Konnov, I., Veith, H., Widder, J.: SMT and POR beat counter abstraction: parameterized model checking of\u00a0threshold-based distributed algorithms. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 85\u2013102. Springer, Heidelberg (2015)"},{"key":"6_CR14","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"crossref","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. 3632, pp. 260\u2013277. Springer, Heidelberg (2005)"},{"issue":"3","key":"6_CR15","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1007\/s10817-006-9042-1","volume":"36","author":"V Kuncak","year":"2006","unstructured":"Kuncak, V., Nguyen, H.H., Rinard, M.: Deciding boolean algebra with Presburger arithmetic. J. Autom. Reasoning 36(3), 213\u2013239 (2006)","journal-title":"J. Autom. Reasoning"},{"key":"6_CR16","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"crossref","first-page":"215","DOI":"10.1007\/978-3-540-73595-3_15","volume-title":"Automated Deduction \u2013 CADE-21","author":"V Kuncak","year":"2007","unstructured":"Kuncak, V., Rinard, M.: Towards efficient satisfiability checking for boolean algebra with Presburger arithmetic. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 215\u2013230. Springer, Heidelberg (2007)"},{"key":"6_CR17","doi-asserted-by":"crossref","unstructured":"Papamarcos, M.S., Patel, J.H.: A low-overhead coherence solution for multiprocessors with private cache memories. In: Proceedings of ISCA, p. 348 (1984)","DOI":"10.1145\/800015.808204"},{"key":"6_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"218","DOI":"10.1007\/978-3-540-78163-9_20","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"R Piskac","year":"2008","unstructured":"Piskac, R., Kuncak, V.: Decision procedures for multisets with cardinality constraints. In: Logozzo, F., Peled, D.A., Zuck, L.D. (eds.) VMCAI 2008. LNCS, vol. 4905, pp. 218\u2013232. Springer, Heidelberg (2008)"},{"key":"6_CR19","first-page":"1","volume":"6","author":"N Schweikhart","year":"2004","unstructured":"Schweikhart, N.: Arithmetic, first-order logic, and counting quantifiers. ACM TOCL 6, 1\u201335 (2004)","journal-title":"ACM TOCL"},{"key":"6_CR20","unstructured":"Solihin, Y.: Fundamentals of Parallel Computer Architecture Multichip and Multicore Systems. Solihin Publishing & Consulting LLC (2008)"},{"issue":"3","key":"6_CR21","doi-asserted-by":"crossref","first-page":"626","DOI":"10.1145\/28869.28876","volume":"34","author":"TK Srikanth","year":"1987","unstructured":"Srikanth, T.K., Toueg, S.: Optimal clock synchronization. J. ACM 34(3), 626\u2013645 (1987)","journal-title":"J. ACM"},{"issue":"2","key":"6_CR22","doi-asserted-by":"crossref","first-page":"80","DOI":"10.1007\/BF01667080","volume":"2","author":"TK Srikanth","year":"1987","unstructured":"Srikanth, T.K., Toueg, S.: Simulating authenticated broadcasts to derive simple fault-tolerant algorithms. Distrib. Comput. 2(2), 80\u201394 (1987)","journal-title":"Distrib. Comput."},{"key":"6_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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. 5944, pp. 380\u2013395. Springer, Heidelberg (2010)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-40229-1_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,24]],"date-time":"2017-06-24T12:12:43Z","timestamp":1498306363000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-40229-1_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319402284","9783319402291"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-40229-1_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}