{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T06:15:02Z","timestamp":1784182502785,"version":"3.55.0"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662488980","type":"print"},{"value":"9783662488997","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-48899-7_25","type":"book-chapter","created":{"date-parts":[[2015,11,21]],"date-time":"2015-11-21T03:59:28Z","timestamp":1448078368000},"page":"356-371","source":"Crossref","is-referenced-by-count":1,"title":["Abstract Domains and Solvers for Sets Reasoning"],"prefix":"10.1007","author":[{"given":"Arlen","family":"Cox","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Bor-Yuh Evan","family":"Chang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Huisong","family":"Li","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Xavier","family":"Rival","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2015,11,22]]},"reference":[{"key":"25_CR1","doi-asserted-by":"crossref","unstructured":"Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: A static analyzer for large safety-critical software. In: PLDI (2003)","DOI":"10.1145\/781131.781153"},{"key":"25_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-27940-9_1","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A Bouajjani","year":"2012","unstructured":"Bouajjani, A., Dr\u0103goi, C., Enea, C., Sighireanu, M.: Abstract domains for automated reasoning about list-manipulating programs with infinite data. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 1\u201322. Springer, Heidelberg (2012)"},{"key":"25_CR3","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":"AR 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. 3855, pp. 427\u2013442. Springer, Heidelberg (2006)"},{"issue":"2","key":"25_CR4","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"EM Clarke","year":"1986","unstructured":"Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. TOPLAS 8(2), 244\u2013263 (1986)","journal-title":"TOPLAS"},{"key":"25_CR5","unstructured":"Coudert, O., Madre, J.C.: A new method to compute prime and essential prime implicants of boolean functions. In: Advanced research in VLSI and Parallel Systems. MIT (1992)"},{"key":"25_CR6","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL (1977)","DOI":"10.1145\/512950.512973"},{"key":"25_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"483","DOI":"10.1007\/978-3-662-46669-8_20","volume-title":"Programming Languages and Systems","author":"A Cox","year":"2015","unstructured":"Cox, A., Chang, B.-Y.E., Rival, X.: Desynchronized multi-state abstractions for open programs in dynamic languages. In: Vitek, J. (ed.) ESOP 2015. LNCS, vol. 9032, pp. 483\u2013509. Springer, Heidelberg (2015)"},{"key":"25_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"866","DOI":"10.1007\/978-3-319-08867-9_57","volume-title":"Computer Aided Verification","author":"A Cox","year":"2014","unstructured":"Cox, A., Chang, B.-Y.E., Sankaranarayanan, S.: QUICr: a reusable library for parametric abstraction of sets and numbers. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 866\u2013873. Springer, Heidelberg (2014)"},{"key":"25_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/978-3-319-10936-7_9","volume-title":"Static Analysis","author":"A Cox","year":"2014","unstructured":"Cox, A., Chang, B.-Y.E., Rival, X.: Automatic analysis of open objects in dynamic language programs. In: M\u00fcller-Olm, M., Seidl, H. (eds.) Static Analysis. LNCS, vol. 8723, pp. 134\u2013150. Springer, Heidelberg (2014)"},{"key":"25_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1007\/978-3-642-39038-8_17","volume-title":"ECOOP 2013 \u2013 Object-Oriented Programming","author":"A Cox","year":"2013","unstructured":"Cox, A., Chang, B.-Y.E., Sankaranarayanan, S.: QUIC graphs: relational invariant generation for containers. In: Castagna, G. (ed.) ECOOP 2013. LNCS, vol. 7920, pp. 401\u2013425. Springer, Heidelberg (2013)"},{"key":"25_CR11","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":"25_CR12","doi-asserted-by":"crossref","unstructured":"Dillig, I., Dillig, T., Aiken, A.: Precise reasoning for programs using containers. In: POPL (2011)","DOI":"10.1145\/1926385.1926407"},{"key":"25_CR13","unstructured":"Kuncak, V.: Modular Data Structure Verification. Ph.D. thesis, EECS Department, Massachusetts Institute of Technology (2007)"},{"issue":"3","key":"25_CR14","doi-asserted-by":"publisher","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.C.: Deciding boolean algebra with presburger arithmetic. J. Autom. Reason. 36(3), 213\u2013239 (2006)","journal-title":"J. Autom. Reason."},{"key":"25_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/978-3-540-45069-6_15","volume-title":"Computer Aided Verification","author":"SK Lahiri","year":"2003","unstructured":"Lahiri, S.K., Bryant, R.E., Cook, B.: A symbolic approach to predicate abstraction. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 141\u2013153. Springer, Heidelberg (2003)"},{"key":"25_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1007\/978-3-662-48288-9_6","volume-title":"Static Analysis","author":"H Li","year":"2015","unstructured":"Li, H., Rival, X., Chang, B.-Y.E.: Shape analysis for unstructured sharing. In: Blazy, S., Jensen, T. (eds.) SAS 2015. LNCS, vol. 9291, pp. 90\u2013108. Springer, Heidelberg (2015)"},{"key":"25_CR17","unstructured":"Mauborgne, L.: Representation of Sets of Trees for Abstract Interpretation. Ph.D. thesis, \u00c9cole Polytechnique (1999)"},{"key":"25_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-45069-6_1","volume-title":"Computer Aided Verification","author":"KL McMillan","year":"2003","unstructured":"McMillan, K.L.: Interpolation and SAT-based model checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 1\u201313. Springer, Heidelberg (2003)"},{"key":"25_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"656","DOI":"10.1007\/978-3-642-22110-1_53","volume-title":"Computer Aided Verification","author":"T-H Pham","year":"2011","unstructured":"Pham, T.-H., Trinh, M.-T., Truong, A.-H., Chin, W.-N.: FixBag: a fixpoint calculator for quantified bag constraints. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 656\u2013662. Springer, Heidelberg (2011)"},{"key":"25_CR20","unstructured":"Reynolds, J.: Separation logic: a logic for shared mutable data structures. In: LICS. IEEE (2002)"},{"key":"25_CR21","unstructured":"Somenzi, F.: Binary decision diagrams. In: Calculational System Design. IOS Press (1999)"},{"key":"25_CR22","unstructured":"Somenzi, F.: CUDD: CU decision diagram package, version 2.5.0 (2012). \n                    http:\/\/vlsi.colorado.edu\/~fabio\/CUDD\/"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-48899-7_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T19:25:29Z","timestamp":1559330729000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-48899-7_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662488980","9783662488997"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-48899-7_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]}}}