{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T02:05:25Z","timestamp":1784167525187,"version":"3.55.0"},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540705437","type":"print"},{"value":"9783540705451","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-70545-1_25","type":"book-chapter","created":{"date-parts":[[2008,8,12]],"date-time":"2008-08-12T16:07:43Z","timestamp":1218557263000},"page":"268-280","source":"Crossref","is-referenced-by-count":24,"title":["Linear Arithmetic with Stars"],"prefix":"10.1007","author":[{"given":"Ruzica","family":"Piskac","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Viktor","family":"Kuncak","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"25_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"457","DOI":"10.1007\/978-3-540-27813-9_36","volume-title":"Computer Aided Verification","author":"T. Ball","year":"2004","unstructured":"Ball, T., Cook, B., Lahiri, S.K., Zhang, L.: Zapato: Automatic theorem proving for predicate abstraction refinement. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 457\u2013461. Springer, Heidelberg (2004)"},{"key":"25_CR2","doi-asserted-by":"crossref","unstructured":"Ball, T., Majumdar, R., Millstein, T., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: Proc. ACM PLDI (2001)","DOI":"10.1145\/378795.378846"},{"key":"25_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46428-X_25","volume-title":"Fundamental Approaches to Software Engineering","author":"M. Balser","year":"2000","unstructured":"Balser, M., Reif, W., Schellhorn, G., Stenzel, K., Thums, A.: Formal System Development with KIV. In: Maibaum, T.S.E. (ed.) ETAPS 2000 and FASE 2000. LNCS, vol.\u00a01783, Springer, Heidelberg (2000)"},{"issue":"1","key":"25_CR4","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., M\u00e9tayer, D.L.: Programming by multiset transformation. Commun. ACM\u00a036(1), 98\u2013111 (1993)","journal-title":"Commun. ACM"},{"key":"25_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"515","DOI":"10.1007\/978-3-540-27813-9_49","volume-title":"Computer Aided Verification","author":"C. Barrett","year":"2004","unstructured":"Barrett, C., Berezin, S.: CVC Lite: A new implementation of the cooperating validity checker. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 515\u2013518. Springer, Heidelberg (2004)"},{"key":"25_CR6","unstructured":"Basin, D., Friedrich, S.: Combining WS1S and HOL. In: FROCOS. vol. 7 of Studies in Logic and Computation (2000)"},{"key":"25_CR7","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/978-3-540-73595-3_13","volume-title":"Automated Deduction \u2013 CADE-21","author":"L. Moura de","year":"2007","unstructured":"de Moura, L., Bj\u00f8rner, N.: Efficient E-Matching for SMT Solvers. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol.\u00a04603, pp. 183\u2013198. Springer, Heidelberg (2007)"},{"key":"25_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46419-0_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L.A. Dennis","year":"2000","unstructured":"Dennis, L.A., Collins, G., Norrish, M., Boulton, R., Slind, K., Robinson, G., Gordon, M., Melham, T.: The PROSPER Toolkit. In: Schwartzbach, M.I., Graf, S. (eds.) ETAPS 2000 and TACAS 2000. LNCS, vol.\u00a01785, Springer, Heidelberg (2000)"},{"issue":"5","key":"25_CR9","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                    \n                      http:\/\/dx.doi.org\/10.1016\/j.orl.2005.09.008","journal-title":"Operations Research Letters"},{"key":"25_CR10","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-540-73595-3_12","volume-title":"Automated Deduction \u2013 CADE-21","author":"Y. Ge","year":"2007","unstructured":"Ge, Y., Barrett, C., Tinelli, C.: Solving quantified verification conditions using satisfiability modulo theories. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol.\u00a04603, pp. 167\u2013182. Springer, Heidelberg (2007)"},{"issue":"2","key":"25_CR11","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":"25_CR12","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL (2002), \n                    \n                      http:\/\/doi.acm.org\/10.1145\/503272.503279"},{"key":"25_CR13","unstructured":"Kuncak, V.: Modular Data Structure Verification. PhD thesis, EECS Department, Massachusetts Institute of Technology (February 2007)"},{"key":"25_CR14","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)"},{"key":"25_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"475","DOI":"10.1007\/978-3-540-27813-9_40","volume-title":"Computer Aided Verification","author":"S.K. Lahiri","year":"2004","unstructured":"Lahiri, S.K., Seshia, S.A.: The UCLID decision procedure. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 475\u2013478. Springer, Heidelberg (2004)"},{"issue":"1-2","key":"25_CR16","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":"25_CR17","doi-asserted-by":"crossref","unstructured":"McLaughlin, S., Barrett, C., Ge, Y.: Cooperating theorem provers: A case study combining HOL-Light and CVC Lite. In: PDPAR. ENTCS, vol.\u00a0144(2) (2006)","DOI":"10.1016\/j.entcs.2005.12.005"},{"key":"25_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/978-3-540-69738-1_18","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"H.H. Nguyen","year":"2007","unstructured":"Nguyen, H.H., David, C., Qin, S., Chin, W.-N.: Automated verification of shape, size and bag properties via separation logic. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol.\u00a04349, pp. 251\u2013266. Springer, Heidelberg (2007)"},{"key":"25_CR19","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C., Voelker, N.: Multiset theory version 1.30 (Isabelle distribution) (2005), \n                    \n                      http:\/\/isabelle.in.tum.de\/dist\/library\/HOL\/Library\/Multiset.html"},{"issue":"4","key":"25_CR20","doi-asserted-by":"publisher","first-page":"765","DOI":"10.1145\/322276.322287","volume":"28","author":"C.H. Papadimitriou","year":"1981","unstructured":"Papadimitriou, C.H.: On the complexity of integer programming. J. ACM\u00a028(4), 765\u2013768 (1981)","journal-title":"J. ACM"},{"key":"25_CR21","series-title":"Lecture Notes in Computer Science","volume-title":"VMCAI","author":"R. Piskac","year":"2008","unstructured":"Piskac, R., Kuncak, V.: Decision procedures for multisets with cardinality constraints. In: VMCAI. LNCS, vol.\u00a04905. Springer, Heidelberg (2008)"},{"key":"25_CR22","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":"25_CR23","unstructured":"Schwartz, J.T.: On programming: An interim report on the SETL project. Technical report, Courant Institute, New York (1973)"},{"key":"25_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44755-5_3","volume-title":"Theorem Proving in Higher Order Logics","author":"N. Shankar","year":"2001","unstructured":"Shankar, N.: Using decision procedures with a higher-order logic. In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001. LNCS, vol.\u00a02152. Springer, Heidelberg (2001)"},{"key":"25_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","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-70545-1_25.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,3]],"date-time":"2021-05-03T04:21:57Z","timestamp":1620015717000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-70545-1_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540705437","9783540705451"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-70545-1_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[]}}