{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:05:15Z","timestamp":1762459515571,"version":"3.37.3"},"reference-count":38,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2017,4,21]],"date-time":"2017-04-21T00:00:00Z","timestamp":1492732800000},"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":["Form Methods Syst Des"],"published-print":{"date-parts":[[2017,12]]},"DOI":"10.1007\/s10703-017-0279-6","type":"journal-article","created":{"date-parts":[[2017,4,21]],"date-time":"2017-04-21T04:57:31Z","timestamp":1492750651000},"page":"545-574","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["Cardinality constraints for arrays (decidability results and applications)"],"prefix":"10.1007","volume":"51","author":[{"given":"F.","family":"Alberti","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6449-6883","authenticated-orcid":false,"given":"S.","family":"Ghilardi","sequence":"additional","affiliation":[]},{"given":"E.","family":"Pagani","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,4,21]]},"reference":[{"key":"279_CR1","doi-asserted-by":"crossref","unstructured":"Abdulla PA, Cerans K, Jonsson B, Tsay YK (1996) General decidability theorems for infinite-state systems. In: Proc. of LICS, pp 313\u2013321","DOI":"10.1109\/LICS.1996.561359"},{"key":"279_CR2","unstructured":"Abdulla PA, Delzanno G, Henda NB, Rezine A (2007) Regular model checking without transducers. TACAS, LNCS vol 4424, pp 721\u2013736"},{"key":"279_CR3","doi-asserted-by":"crossref","unstructured":"Abdulla PA, Delzanno G, Rezine A (2007) Parameterized verification of infinite-state processes with global conditions. CAV, LNCS, vol 4590, pp 145\u2013157","DOI":"10.1007\/978-3-540-73368-3_17"},{"issue":"2","key":"279_CR4","doi-asserted-by":"crossref","first-page":"91","DOI":"10.1006\/inco.1996.0053","volume":"127","author":"PA Abdulla","year":"1996","unstructured":"Abdulla PA, Jonsson B (1996) Verifying programs with unreliable channels. Inf Comput 127(2):91\u2013101","journal-title":"Inf Comput"},{"key":"279_CR5","doi-asserted-by":"crossref","first-page":"241","DOI":"10.1016\/S0304-3975(01)00330-9","volume":"290","author":"PA Abdulla","year":"2003","unstructured":"Abdulla PA, Jonsson B (2003) Model checking of systems with many identical timed processes. Theor Comput Sci 290:241\u2013264","journal-title":"Theor Comput Sci"},{"key":"279_CR6","doi-asserted-by":"crossref","unstructured":"Alberti F, Ghilardi S, Pagani E (2016) Counting constraints in flat array fragments. In: Automated reasoning\u20148th international joint conference, IJCAR 2016, Coimbra, Portugal, June 27\u2013July 2, 2016, Proceedings, pp 65\u201381","DOI":"10.1007\/978-3-319-40229-1_6"},{"key":"279_CR7","doi-asserted-by":"publisher","unstructured":"Alberti F, Ghilardi S, Sharygina N (2015) Decision procedures for flat array properties. J Autom Reason 54(4):327\u2013352. doi: 10.1007\/s10817-015-9323-7","DOI":"10.1007\/s10817-015-9323-7"},{"key":"279_CR8","doi-asserted-by":"crossref","unstructured":"Bansal K, Reynolds A, Barrett CW, Tinelli C (2016) A new decision procedure for finite sets and cardinality constraints in SMT. In: Automated reasoning\u20148th international joint conference, IJCAR 2016, Coimbra, Portugal, June 27\u2014July 2, 2016, Proceedings, pp 82\u201398","DOI":"10.1007\/978-3-319-40229-1_7"},{"key":"279_CR9","unstructured":"Biely M, Charron-Bost B, Gaillard A, Hutle M, Schiper A (2007) Widder, J.: Tolerating corrupted communication. In: Proc. PODC, pp 244\u2013253"},{"key":"279_CR10","doi-asserted-by":"crossref","unstructured":"Bj\u00f8rner N, von Gleissenthall K, Rybalchenko A (2016) Cardinalities and universal quantifiers for verifying parameterized systems. In: Proc. of the 37th ACM SIGPLAN conference on programming language design and implementation (PLDI)","DOI":"10.1145\/2908080.2908129"},{"key":"279_CR11","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 (2009) The heard-of model: computing in distributed systems with benign faults. Distrib Comput 22:49\u201371","journal-title":"Distrib Comput"},{"key":"279_CR12","doi-asserted-by":"crossref","unstructured":"Delzanno G, Esparza J, Podelski A (1999) Constraint-based analysis of broadcast protocols. In: Proc. of CSL, LNCS, vol 1683, pp 50\u201366","DOI":"10.1007\/3-540-48168-0_5"},{"key":"279_CR13","doi-asserted-by":"crossref","unstructured":"de Moura L, Bj\u00f8rner N (2008) Z3: An efficient SMT solver. In: TACAS, pp 337\u2013340","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"279_CR14","doi-asserted-by":"crossref","unstructured":"Dragoi C, Henzinger T, Veith H, Widder J, Zufferey D (2014) A logic-based framework for verifying consensus algorithms. In: Proc. of VMCAI","DOI":"10.1007\/978-3-642-54013-4_10"},{"key":"279_CR15","unstructured":"Dragoi C, Henzinger T, Zufferey D (2015) The need for language support for fault-tolerant distributed systems. In: Proc. of SNAPL"},{"issue":"5","key":"279_CR16","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 (2006) Carath\u00e9odory bounds for integer cones. Oper Res Lett 34(5):564\u2013568","journal-title":"Oper Res Lett"},{"key":"279_CR17","doi-asserted-by":"crossref","unstructured":"Esparza J, Finkel A, Mayr R (1999) On the verification of broadcast protocols. In: Proc. of LICS. IEEE Computer Society, pp 352\u2013359","DOI":"10.1109\/LICS.1999.782630"},{"key":"279_CR18","doi-asserted-by":"publisher","unstructured":"Ge Y, de Moura LM (2009) Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In: Computer aided verification, 21st international conference, CAV 2009, Grenoble, France, June 26\u2013July 2, 2009. Proceedings, pp 306\u2013320. doi: 10.1007\/978-3-642-02658-4_25","DOI":"10.1007\/978-3-642-02658-4_25"},{"key":"279_CR19","unstructured":"Ghilardi S, Pagani E (2017) Counter systems simulations: a higher-order logic approach, manuscript"},{"issue":"2","key":"279_CR20","doi-asserted-by":"crossref","first-page":"637","DOI":"10.2307\/2274706","volume":"56","author":"J Halpern","year":"1991","unstructured":"Halpern J (1991) Presburger arithmetic with unary predicates is $$\\varPi ^1_1$$ \u03a0 1 1 complete. J Symbo Log 56(2):637\u2013642","journal-title":"J Symbo Log"},{"key":"279_CR21","volume-title":"The art of multiprocessor programming","author":"M Herlihy","year":"2008","unstructured":"Herlihy M, Shavit N (2008) The art of multiprocessor programming. Morgan Kaufmann, Burlington"},{"key":"279_CR22","doi-asserted-by":"crossref","unstructured":"John A, Konnov I, Schmid U, Veith H, Widder J (2013) Parameterized model checking of fault-tolerant distributed algorithms by abstraction. In: Proc. of FMCAD, pp 201\u2013209","DOI":"10.1109\/FMCAD.2013.6679411"},{"key":"279_CR23","doi-asserted-by":"publisher","unstructured":"Konnov I, Veith H, Widder J (2015) SMT and POR beat counter abstraction: parameterized model checking of threshold-based distributed algorithms. In: Computer aided verification, 27th international conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I, pp 85\u2013102. doi: 10.1007\/978-3-319-21690-4_6","DOI":"10.1007\/978-3-319-21690-4_6"},{"key":"279_CR24","doi-asserted-by":"publisher","unstructured":"Konnov IV, Veith H, Widder J (2017) On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability. Inf Comput 252:95\u2013109. doi: 10.1016\/j.ic.2016.03.006","DOI":"10.1016\/j.ic.2016.03.006"},{"key":"279_CR25","unstructured":"Konnov IV, Veith H, Widder J (2015) What you always wanted to know about model checking of fault-tolerant distributed algorithms. In: Perspectives of system informatics\u201410th international Andrei Ershov informatics conference, PSI 2015, in Memory of Helmut Veith, Kazan and Innopolis, Russia, August 24\u201327, 2015, Revised Selected Papers, pp 6\u201321"},{"key":"279_CR26","doi-asserted-by":"crossref","unstructured":"Kuncak V, Nguyen H, Rinard M (2005) An algorithm for deciding BAPA: Boolean Algebra with Presburger Arithmetic. In: Proc. of CADE-20, LNCS, vol 3632","DOI":"10.1007\/11532231_20"},{"issue":"3","key":"279_CR27","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 HH, Rinard M (2006) Deciding Boolean algebra with Presburger arithmetic. J Autom Reason 36(3):213\u2013239","journal-title":"J Autom Reason"},{"key":"279_CR28","doi-asserted-by":"crossref","unstructured":"Kunkak V, Rinard M (2007) Towards efficient satisfiability checking for Boolean Algebras with Presburger arithmetic. In: CADE, vol 21, pp 215\u2013230","DOI":"10.1007\/978-3-540-73595-3_15"},{"issue":"6","key":"279_CR29","doi-asserted-by":"crossref","first-page":"937","DOI":"10.1145\/1217856.1217859","volume":"53","author":"R Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis R, Oliveras A, Tinelli C (2006) Solving SAT and SAT modulo theories: from an abstract davis-putnam-logemann-loveland procedure to DPLL(T). J ACM 53(6):937\u2013977","journal-title":"J ACM"},{"key":"279_CR30","doi-asserted-by":"crossref","unstructured":"Papamarcos M, Patel J (1984) A low-overhead coherence solution for multiprocessors with private cache memories. In: Proc. ISCA, p 348","DOI":"10.1145\/800015.808204"},{"key":"279_CR31","doi-asserted-by":"crossref","unstructured":"Piskac R, Kuncak V (2008) Decision procedures for multisets with cardinality constraints. In: Proc. of VMCAI, LNCS","DOI":"10.1007\/978-3-540-78163-9_20"},{"key":"279_CR32","unstructured":"Presburger M (1929) \u00dcber die Vollst\u00e4ndigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. Warszawa"},{"key":"279_CR33","unstructured":"Schweikhart N (2004) Arithmetic, first-order logic, and counting quantifiers. ACM TOCL pp 1\u201335"},{"key":"279_CR34","volume-title":"Fundamentals of parallel computer architecture multichip and multicore systems","author":"Y Solihin","year":"2008","unstructured":"Solihin Y (2008) Fundamentals of parallel computer architecture multichip and multicore systems. Solihin Publishing & Consulting LLC, Raleigh"},{"issue":"3","key":"279_CR35","doi-asserted-by":"crossref","first-page":"626","DOI":"10.1145\/28869.28876","volume":"34","author":"T Srikanth","year":"1987","unstructured":"Srikanth T, Toueg S (1987) Optimal clock synchronization. J ACM 34(3):626\u2013645","journal-title":"J ACM"},{"issue":"2","key":"279_CR36","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1007\/BF01667080","volume":"2","author":"T Srikanth","year":"1987","unstructured":"Srikanth T, Toueg S (1987) Simulating authenticated broadcasts to derive simple fault-tolerant algorithms. Distrib Comput 2(2):80\u201394. doi: 10.1007\/BF01667080","journal-title":"Distrib Comput"},{"key":"279_CR37","doi-asserted-by":"crossref","unstructured":"Yessenov K, Piskac R, Kuncak V (2010) Collections, cardinalities, and relations. In: Proc. of VMCAI","DOI":"10.1007\/978-3-642-11319-2_27"},{"key":"279_CR38","doi-asserted-by":"crossref","unstructured":"Zarba C (2002) Combining sets with integers. In: Frontiers of combining systems, 4th international workshop, FroCoS 2002, Santa Margherita Ligure, Italy, April 8\u201310, Proceedings, pp 103\u2013116","DOI":"10.1007\/3-540-45988-X_9"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-017-0279-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-017-0279-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-017-0279-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,21]],"date-time":"2019-09-21T09:45:20Z","timestamp":1569059120000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-017-0279-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,4,21]]},"references-count":38,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2017,12]]}},"alternative-id":["279"],"URL":"https:\/\/doi.org\/10.1007\/s10703-017-0279-6","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2017,4,21]]}}}