{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T13:29:24Z","timestamp":1725542964373},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642113185"},{"type":"electronic","value":"9783642113192"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-11319-2_27","type":"book-chapter","created":{"date-parts":[[2010,1,6]],"date-time":"2010-01-06T05:00:05Z","timestamp":1262754005000},"page":"380-395","source":"Crossref","is-referenced-by-count":21,"title":["Collections, Cardinalities, and Relations"],"prefix":"10.1007","author":[{"given":"Kuat","family":"Yessenov","sequence":"first","affiliation":[]},{"given":"Ruzica","family":"Piskac","sequence":"additional","affiliation":[]},{"given":"Viktor","family":"Kuncak","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"27_CR1","unstructured":"Baader, F., Calvanese, D., McGuinness, D., Nardi, D., Patel-Schneider, P. (eds.): The Description Logic Handbook: Theory, Implementation and Applications. CUP (2003)"},{"key":"27_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1007\/978-3-540-70592-5_17","volume-title":"ECOOP 2008 \u2013 Object-Oriented Programming","author":"A. Banerjee","year":"2008","unstructured":"Banerjee, A., Naumann, D.A., Rosenberg, S.: Regional logic for local reasoning about global invariants. In: Vitek, J. (ed.) ECOOP 2008. LNCS, vol.\u00a05142, pp. 387\u2013411. Springer, Heidelberg (2008)"},{"key":"27_CR3","doi-asserted-by":"crossref","unstructured":"Barnett, M., Leino, K.R.M.: Weakest-precondition of unstructured programs. In: PASTE, pp. 82\u201387 (2005)","DOI":"10.1145\/1108792.1108813"},{"issue":"5-6","key":"27_CR4","doi-asserted-by":"publisher","first-page":"505","DOI":"10.1007\/s10009-007-0044-z","volume":"9","author":"D. Beyer","year":"2007","unstructured":"Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: The software model checker BLAST. STTT\u00a09(5-6), 505\u2013525 (2007)","journal-title":"STTT"},{"key":"27_CR5","series-title":"Lecture Notes in Computer Science","volume-title":"TPHOLs 2009","author":"E. Cohen","year":"2009","unstructured":"Cohen, E., Dahlweid, M., Hillebrand, M., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: VCC: A practical system for verifying concurrent c. In: TPHOLs 2009. LNCS, vol.\u00a05674. Springer, Heidelberg (2009)"},{"key":"27_CR6","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: POPL (1979)","DOI":"10.1145\/567752.567778"},{"key":"27_CR7","doi-asserted-by":"crossref","unstructured":"Dewar, R.K.: Programming by refinement, as exemplified by the SETL representation sublanguage. In: ACM TOPLAS (July 1979)","DOI":"10.1145\/357062.357064"},{"issue":"5","key":"27_CR8","doi-asserted-by":"publisher","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. Operations Research Letters\u00a034(5), 564\u2013568 (2006)","journal-title":"Operations Research Letters"},{"key":"27_CR9","doi-asserted-by":"crossref","first-page":"57","DOI":"10.4064\/fm-47-1-57-103","volume":"47","author":"S. Feferman","year":"1959","unstructured":"Feferman, S., Vaught, R.L.: The first order properties of products of algebraic systems. Fundamenta Mathematicae\u00a047, 57\u2013103 (1959)","journal-title":"Fundamenta Mathematicae"},{"issue":"2","key":"27_CR10","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1006\/inco.2001.2973","volume":"174","author":"R. Givan","year":"2002","unstructured":"Givan, R., McAllester, D., Witty, C., Kozen, D.: Tarskian set constraints. Inf. Comput.\u00a0174(2), 105\u2013131 (2002)","journal-title":"Inf. Comput."},{"key":"27_CR11","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Lev-Ami, T., Sagiv, M.: A combination framework for tracking partition sizes. In: POPL 2009, pp. 239\u2013251 (2009)","DOI":"10.1145\/1594834.1480912"},{"key":"27_CR12","doi-asserted-by":"crossref","unstructured":"Gurevich, Y., Shelah, S.: Spectra of monadic second-order formulas with one unary function. In: LICS, pp. 291\u2013300 (2003)","DOI":"10.1109\/LICS.2003.1210069"},{"key":"27_CR13","doi-asserted-by":"crossref","unstructured":"Kuncak, V., Lam, P., Zee, K., Rinard, M.: Modular pluggable analyses for data structure consistency. IEEE Trans. Software Engineering\u00a032(12) (December 2006)","DOI":"10.1109\/TSE.2006.125"},{"key":"27_CR14","doi-asserted-by":"crossref","unstructured":"Kuncak, V., Nguyen, H.H., Rinard, M.: Deciding Boolean Algebra with Presburger Arithmetic. J. of Automated Reasoning (2006)","DOI":"10.1007\/s10817-006-9042-1"},{"key":"27_CR15","doi-asserted-by":"crossref","unstructured":"Kuncak, V., Rinard, M.: Decision procedures for set-valued fields. In: 1st International Workshop on Abstract Interpretation of Object-Oriented Languages (2005)","DOI":"10.1016\/j.entcs.2005.01.022"},{"key":"27_CR16","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","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.\u00a04603, pp. 215\u2013230. Springer, Heidelberg (2007)"},{"issue":"3","key":"27_CR17","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1016\/0022-0000(80)90027-6","volume":"21","author":"H.R. Lewis","year":"1980","unstructured":"Lewis, H.R.: Complexity results for classes of quantificational formulas. J. Comput. Syst. Sci.\u00a021(3), 317\u2013353 (1980)","journal-title":"J. Comput. Syst. Sci."},{"issue":"2","key":"27_CR18","first-page":"354","volume":"11","author":"Y.V. Matiyasevich","year":"1970","unstructured":"Matiyasevich, Y.V.: Enumerable sets are Diophantine. Soviet Math. Doklady\u00a011(2), 354\u2013357 (1970)","journal-title":"Soviet Math. Doklady"},{"key":"27_CR19","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/S0004-3702(99)00011-9","volume":"109","author":"H.J. Ohlbach","year":"1999","unstructured":"Ohlbach, H.J., Koehler, J.: Modal logics, description logics and arithmetic reasoning. Artificial Intelligence\u00a0109, 1\u201331 (1999)","journal-title":"Artificial Intelligence"},{"issue":"4","key":"27_CR20","doi-asserted-by":"publisher","first-page":"1083","DOI":"10.1137\/S0097539797323005","volume":"29","author":"L. Pacholski","year":"2000","unstructured":"Pacholski, L., Szwast, W., Tendera, L.: Complexity results for first-order two-variable logic with counting. SIAM J. on Computing\u00a029(4), 1083\u20131117 (2000)","journal-title":"SIAM J. on Computing"},{"key":"27_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"584","DOI":"10.1007\/978-3-642-02658-4_43","volume-title":"CAV 2009","author":"J.A.N. P\u00e9rez","year":"2009","unstructured":"P\u00e9rez, J.A.N., Rybalchenko, A., Singh, A.: Cardinality abstraction for declarative networking applications. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 584\u2013598. Springer, Heidelberg (2009)"},{"key":"27_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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.\u00a04905, pp. 218\u2013232. Springer, Heidelberg (2008)"},{"key":"27_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/978-3-540-70545-1_25","volume-title":"Computer Aided Verification","author":"R. Piskac","year":"2008","unstructured":"Piskac, R., Kuncak, V.: Linear arithmetic with stars. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 268\u2013280. Springer, Heidelberg (2008)"},{"issue":"3","key":"27_CR24","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1007\/s10849-005-5791-1","volume":"14","author":"I. Pratt-Hartmann","year":"2005","unstructured":"Pratt-Hartmann, I.: Complexity of the two-variable fragment with counting quantifiers. Journal of Logic, Language and Information\u00a014(3), 369\u2013395 (2005)","journal-title":"Journal of Logic, Language and Information"},{"key":"27_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"252","DOI":"10.1007\/978-3-540-24622-0_21","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"T. Reps","year":"2004","unstructured":"Reps, T., Sagiv, M., Yorsh, G.: Symbolic implementation of the best transformer. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol.\u00a02937, pp. 252\u2013266. Springer, Heidelberg (2004)"},{"issue":"59","key":"27_CR26","first-page":"1","volume":"9","author":"J. Venn","year":"1880","unstructured":"Venn, J.: On the diagrammatic and mechanical representation of propositions and reasonings. Dublin Philosophical Magazine and Journal of Science\u00a09(59), 1\u201318 (1880)","journal-title":"Dublin Philosophical Magazine and Journal of Science"},{"key":"27_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/11609773_11","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"T. Wies","year":"2005","unstructured":"Wies, T., Kuncak, V., Lam, P., Podelski, A., Rinard, M.: Field constraint analysis. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol.\u00a03855, pp. 157\u2013173. Springer, Heidelberg (2005)"},{"key":"27_CR28","series-title":"LNAI","first-page":"366","volume-title":"FroCos 2009","author":"T. Wies","year":"2009","unstructured":"Wies, T., Piskac, R., Kuncak, V.: Combining theories with shared set operations. In: Ghilardi, S., Sebastiani, R. (eds.) FroCoS 2009. LNCS (LNAI), vol.\u00a05749, pp. 366\u2013382. Springer, Heidelberg (2009)"},{"key":"27_CR29","doi-asserted-by":"crossref","unstructured":"Zee, K., Kuncak, V., Rinard, M.: Full functional verification of linked data structures. In: ACM PLDI (2008)","DOI":"10.1145\/1375581.1375624"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-11319-2_27.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T02:39:31Z","timestamp":1606185571000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-11319-2_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642113185","9783642113192"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-11319-2_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}