{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,14]],"date-time":"2026-03-14T18:16:19Z","timestamp":1773512179316,"version":"3.50.1"},"publisher-location":"Cham","reference-count":14,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319402284","type":"print"},{"value":"9783319402291","type":"electronic"}],"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_7","type":"book-chapter","created":{"date-parts":[[2016,6,11]],"date-time":"2016-06-11T08:54:04Z","timestamp":1465635244000},"page":"82-98","source":"Crossref","is-referenced-by-count":23,"title":["A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT"],"prefix":"10.1007","author":[{"given":"Kshitij","family":"Bansal","sequence":"first","affiliation":[]},{"given":"Andrew","family":"Reynolds","sequence":"additional","affiliation":[]},{"given":"Clark","family":"Barrett","sequence":"additional","affiliation":[]},{"given":"Cesare","family":"Tinelli","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,6,12]]},"reference":[{"key":"7_CR1","doi-asserted-by":"crossref","unstructured":"Bansal, K.: Decision Procedures for Finite Sets with Cardinality and Local Theory Extensions. Ph.D. thesis, New York University, January 2016","DOI":"10.1007\/978-3-319-40229-1_7"},{"key":"7_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1007\/978-3-642-22110-1_14","volume-title":"Computer Aided Verification","author":"C Barrett","year":"2011","unstructured":"Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanovi\u0107, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171\u2013177. Springer, Heidelberg (2011)"},{"key":"7_CR3","unstructured":"Barrett, C., Sebastiani, R., Seshia, S., Tinelli, C.: Satisfiability modulo theories. In: Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, vol. 185, pp. 825\u2013885, chapter 26. IOS Press, February 2009"},{"key":"7_CR4","doi-asserted-by":"crossref","unstructured":"Blanc, R.W., Kneuss, E., Kuncak, V., Suter, P.: An overview of the Leon verification system: verification by translation to recursive functions. In: Scala Workshop (2013)","DOI":"10.1145\/2489837.2489838"},{"key":"7_CR5","series-title":"Monographs in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4757-3452-2","volume-title":"Set Theory for Computing: From Decision Procedures to Logic Programming with Sets","author":"D Cantone","year":"2001","unstructured":"Cantone, D., Omodeo, E.G., Policriti, A.: Set Theory for Computing: From Decision Procedures to Logic Programming with Sets. Monographs in Computer Science. Springer, Heidelberg (2001)"},{"key":"7_CR6","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"crossref","first-page":"126","DOI":"10.1007\/3-540-46508-1_8","volume-title":"Automated Deduction in Classical and Non-Classical Logics","author":"D Cantone","year":"2000","unstructured":"Cantone, D., Zarba, C.G.: A new fast tableau-based decision procedure for an unquantified fragment of set theory. In: Caferra, R., Salzer, G. (eds.) FTP 1998. LNCS (LNAI), vol. 1761, pp. 126\u2013136. Springer, Heidelberg (2000)"},{"key":"7_CR7","doi-asserted-by":"crossref","unstructured":"De Moura, L., Bj\u00f8rner, N.: Generalized, efficient array decision procedures. In: Formal Methods in Computer-Aided Design (FMCAD 2009), pp. 45\u201352. IEEE (2009)","DOI":"10.1109\/FMCAD.2009.5351142"},{"key":"7_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"402","DOI":"10.1007\/978-3-642-16242-8_29","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"D Jovanovi\u0107","year":"2010","unstructured":"Jovanovi\u0107, D., Barrett, C.: Polite theories revisited. In: Ferm\u00fcller, C.G., Voronkov, A. (eds.) LPAR-17. LNCS, vol. 6397, pp. 402\u2013416. Springer, Heidelberg (2010)"},{"key":"7_CR9","unstructured":"Kr\u00f6ning, D., R\u00fcmmer, P., Weissenbacher, G.: A proposal for a theory of finite sets, lists, and maps for the SMT-LIB standard. In: Proceedings of the 7 $$^th$$ International Workshop on Satisfiability Modulo Theories (SMT 2009), August 2009"},{"issue":"3","key":"7_CR10","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":"7_CR11","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)"},{"issue":"6","key":"7_CR12","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.: Solving SAT and SAT Modulo theories: from an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). J. ACM 53(6), 937\u2013977 (2006)","journal-title":"J. ACM"},{"key":"7_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"403","DOI":"10.1007\/978-3-642-18275-4_28","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"P Suter","year":"2011","unstructured":"Suter, P., Steiger, R., Kuncak, V.: Sets with cardinality constraints in satisfiability modulo theories. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 403\u2013418. Springer, Heidelberg (2011)"},{"key":"7_CR14","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1007\/3-540-45988-X_9","volume-title":"Frontiers of Combining Systems","author":"CG Zarba","year":"2002","unstructured":"Zarba, C.G.: Combining sets with integers. In: Armando, A. (ed.) FroCos 2002. LNCS (LNAI), vol. 2309, pp. 103\u2013116. Springer, Heidelberg (2002)"}],"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_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,9]],"date-time":"2019-09-09T12:38:34Z","timestamp":1568032714000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-40229-1_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319402284","9783319402291"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-40229-1_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]}}}