{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T14:44:12Z","timestamp":1742913852384,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540875307"},{"type":"electronic","value":"9783540875314"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2008]]},"DOI":"10.1007\/978-3-540-87531-4_11","type":"book-chapter","created":{"date-parts":[[2008,8,30]],"date-time":"2008-08-30T08:40:53Z","timestamp":1220085653000},"page":"124-138","source":"Crossref","is-referenced-by-count":6,"title":["Fractional Collections with Cardinality Bounds, and Mixed Linear Arithmetic with Stars"],"prefix":"10.1007","author":[{"given":"Ruzica","family":"Piskac","sequence":"first","affiliation":[]},{"given":"Viktor","family":"Kuncak","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"11_CR1","doi-asserted-by":"crossref","unstructured":"Berezin, S., Ganesh, V., Dill, D.L.: An online proof-producing decision procedure for mixed-integer linear arithmetic. In: TACAS (2003)","DOI":"10.1007\/3-540-36577-X_38"},{"key":"11_CR2","volume-title":"The Calculus of Computation","author":"A.R. Bradley","year":"2007","unstructured":"Bradley, A.R., Manna, Z.: The Calculus of Computation. Springer, Heidelberg (2007)"},{"key":"11_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/11817963_11","volume-title":"Computer Aided Verification","author":"B. Dutertre","year":"2006","unstructured":"Dutertre, B., de Moura, L.: A Fast Linear-Arithmetic Solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 81\u201394. Springer, Heidelberg (2006)"},{"key":"11_CR4","unstructured":"Dutertre, B., de Moura, L.: Integrating Simplex with DPLL(T). Technical Report SRI-CSL-06-01, SRI International (2006)"},{"issue":"5","key":"11_CR5","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), \n                      http:\/\/dx.doi.org\/10.1016\/j.orl.2005.09.008","journal-title":"Operations Research Letters"},{"key":"11_CR6","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":"11_CR7","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":"11_CR8","doi-asserted-by":"crossref","unstructured":"Kuncak, V., Nguyen, H.H., Rinard, M.: Deciding Boolean Algebra with Presburger Arithmetic. J. of Automated Reasoning (2006), \n                      http:\/\/dx.doi.org\/10.1007\/s10817-006-9042-1","DOI":"10.1007\/s10817-006-9042-1"},{"key":"11_CR9","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":"1-2","key":"11_CR10","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":"11_CR11","unstructured":"Lugiez, D., Zilio, S.D.: Multitrees Automata, Presburger\u2019s Constraints and Tree Logics. Research report 08-2002, LIF, Marseille, France (June 2002), \n                      http:\/\/www.lif-sud.univ-mrs.fr\/Rapports\/08-2002.html"},{"key":"11_CR12","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":"11_CR13","unstructured":"Piskac, R., Kuncak, V.: Linear arithmetic with stars. In: CAV (2008)"},{"key":"11_CR14","unstructured":"Piskac, R., Kuncak, V.: On linear arithmetic with stars. Technical Report LARA-REPORT-2008-005, EPFL (2008)"},{"key":"11_CR15","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":"11_CR16","doi-asserted-by":"crossref","unstructured":"Pugh, W.: The Omega test: a fast and practical integer programming algorithm for dependence analysis. In: ACM\/IEEE conf. Supercomputing (1991)","DOI":"10.1145\/125826.125848"},{"key":"11_CR17","volume-title":"Theory of Linear and Integer Programming","author":"A. Schrijver","year":"1998","unstructured":"Schrijver, A.: Theory of Linear and Integer Programming. John Wiley & Sons, Chichester (1998)"},{"key":"11_CR18","doi-asserted-by":"crossref","unstructured":"Weispfenning, V.: Mixed real-integer linear quantifier elimination. In: ISSAC, pp. 129\u2013136 (1999)","DOI":"10.1145\/309831.309888"},{"key":"11_CR19","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1016\/S0019-9958(65)90241-X","volume":"8","author":"L.A. Zadeh","year":"1965","unstructured":"Zadeh, L.A.: Fuzzy sets. Information and Control\u00a08, 338\u2013353 (1965)","journal-title":"Information and Control"},{"key":"11_CR20","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","Computer Science Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-87531-4_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,5,7]],"date-time":"2024-05-07T05:12:17Z","timestamp":1715058737000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-540-87531-4_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540875307","9783540875314"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-87531-4_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}