{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,4]],"date-time":"2025-04-04T01:47:21Z","timestamp":1743731241436},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540781622"},{"type":"electronic","value":"9783540781639"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-78163-9_20","type":"book-chapter","created":{"date-parts":[[2008,2,29]],"date-time":"2008-02-29T05:30:06Z","timestamp":1204263006000},"page":"218-232","source":"Crossref","is-referenced-by-count":22,"title":["Decision Procedures for Multisets with Cardinality Constraints"],"prefix":"10.1007","author":[{"given":"Ruzica","family":"Piskac","sequence":"first","affiliation":[]},{"given":"Viktor","family":"Kuncak","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"20_CR1","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1016\/S0167-6423(99)00007-6","volume":"35","author":"A. Aiken","year":"1999","unstructured":"Aiken, A.: Introduction to set constraint-based program analysis. Science of Computer Programming\u00a035, 79\u2013111 (1999)","journal-title":"Science of Computer Programming"},{"issue":"1","key":"20_CR2","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1145\/151233.151242","volume":"36","author":"J.-P. Ban\u00e2tre","year":"1993","unstructured":"Ban\u00e2tre, J.-P., Le M\u00e9tayer, D.: Programming by multiset transformation. Commun. ACM\u00a036(1), 98\u2013111 (1993)","journal-title":"Commun. ACM"},{"key":"20_CR3","doi-asserted-by":"publisher","first-page":"197","DOI":"10.4064\/fm171-3-1","volume":"171","author":"A. B\u00e8s","year":"2002","unstructured":"B\u00e8s, A.: Definability and decidability results related to the elementary theory of ordinal multiplication. Fund. Math.\u00a0171, 197\u2013211 (2002)","journal-title":"Fund. Math."},{"key":"20_CR4","doi-asserted-by":"crossref","unstructured":"Domenjoud, E.: Solving systems of linear diophantine equations: An algebraic approach. In: MFCS, pp. 141\u2013150 (1991)","DOI":"10.1007\/3-540-54345-7_57"},{"issue":"3","key":"20_CR5","doi-asserted-by":"publisher","first-page":"496","DOI":"10.1016\/j.tcs.2005.03.012","volume":"340","author":"A. Durand","year":"2005","unstructured":"Durand, A., Hermann, M., Kolaitis, P.G.: Subtractive reductions and complete problems for counting complexity classes. Theor. Comput. Sci.\u00a0340(3), 496\u2013513 (2005)","journal-title":"Theor. Comput. Sci."},{"issue":"5","key":"20_CR6","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":"20_CR7","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":"20_CR8","doi-asserted-by":"crossref","first-page":"285","DOI":"10.2140\/pjm.1966.16.285","volume":"16","author":"S. Ginsburg","year":"1966","unstructured":"Ginsburg, S., Spanier, E.: Semigroups, Pressburger formulas and languages. Pacific Journal of Mathematics\u00a016(2), 285\u2013296 (1966)","journal-title":"Pacific Journal of Mathematics"},{"key":"20_CR9","unstructured":"Kuncak, V.: Modular Data Structure Verification. PhD thesis, EECS Department, Massachusetts Institute of Technology (February 2007)"},{"key":"20_CR10","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":"20_CR11","unstructured":"Kuncak, V., Rinard, M.: On the theory of structural subtyping. Technical Report 879, LCS, Massachusetts Institute of Technology (2003)"},{"key":"20_CR12","doi-asserted-by":"crossref","unstructured":"Kuncak, V., Rinard, M.: Towards efficient satisfiability checking for Boolean Algebra with Presburger Arithmetic. In: CADE-21 (2007)","DOI":"10.1007\/978-3-540-73595-3_15"},{"issue":"1-2","key":"20_CR13","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1016\/j.tcs.2004.10.023","volume":"333","author":"D. Lugiez","year":"2005","unstructured":"Lugiez, D.: Multitree automata that count. Theor. Comput. Sci.\u00a0333(1-2), 225\u2013263 (2005)","journal-title":"Theor. Comput. Sci."},{"key":"20_CR14","unstructured":"Lugiez, D., Zilio, S.D.: Multitrees Automata, Presburger\u2019s Constraints and Tree Logics. Research report 08-2002, LIF, Marseille, France (June 2002), http:\/\/www.lif-sud.univ-mrs.fr\/Rapports\/08-2002.html"},{"key":"20_CR15","unstructured":"Marnette, B., Kuncak, V., Rinard, M.: On algorithms and complexity for sets with cardinality constraints. Technical report, MIT CSAIL (August 2005)"},{"issue":"2","key":"20_CR16","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"},{"issue":"2","key":"20_CR17","first-page":"239","volume":"3","author":"J. Misra","year":"1995","unstructured":"Misra, J.: A logic for concurrent programming (in two parts): Safety and progress. Journal of Computer and Software Engineering\u00a03(2), 239\u2013300 (1995)","journal-title":"Journal of Computer and Software Engineering"},{"key":"20_CR18","unstructured":"Nguyen, H.H., et al.: Automated verification of shape, size and bag properties via separation logic. In: VMCAI (2007)"},{"key":"20_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"20_CR20","unstructured":"Nipkow, T., et al.: Multiset theory version 1.30 (Isabelle distribution) (2005), http:\/\/isabelle.in.tum.de\/dist\/library\/HOL\/Library\/Multiset.html"},{"issue":"4","key":"20_CR21","doi-asserted-by":"publisher","first-page":"765","DOI":"10.1145\/322276.322287","volume":"28","author":"H. Christos","year":"1981","unstructured":"Christos, H., Papadimitriou, C.H.: On the complexity of integer programming. J. ACM\u00a028(4), 765\u2013768 (1981)","journal-title":"J. ACM"},{"issue":"5","key":"20_CR22","doi-asserted-by":"publisher","first-page":"626","DOI":"10.1145\/504709.504711","volume":"23","author":"L.C. Paulson","year":"2001","unstructured":"Paulson, L.C.: Mechanizing a theory of program composition for UNITY. ACM Trans. Program. Lang. Syst.\u00a023(5), 626\u2013656 (2001)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"20_CR23","series-title":"Lecture Notes in Computer Science","volume-title":"Rewriting Techniques and Applications","author":"L. Pottier","year":"1991","unstructured":"Pottier, L.: Minimal solutions of linear diophantine systems: Bounds and algorithms. In: Book, R.V. (ed.) RTA 1991. LNCS, vol.\u00a0488, Springer, Heidelberg (1991)"},{"key":"20_CR24","unstructured":"Schwartz, J.T.: On programming: An interim report on the SETL project. Technical report, Courant Institute, New York (1973)"},{"key":"20_CR25","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Automated Deduction - CADE-18","author":"C.G. Zarba","year":"2002","unstructured":"Zarba, C.G.: Combining multisets with integers. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol.\u00a02392, Springer, Heidelberg (2002)"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-78163-9_20.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T07:00:35Z","timestamp":1619506835000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-78163-9_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540781622","9783540781639"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-78163-9_20","relation":{},"subject":[]}}