{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:54:00Z","timestamp":1762458840652,"version":"3.37.3"},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642152047"},{"type":"electronic","value":"9783642152054"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-15205-4_5","type":"book-chapter","created":{"date-parts":[[2010,8,13]],"date-time":"2010-08-13T14:48:24Z","timestamp":1281710904000},"page":"34-48","source":"Crossref","is-referenced-by-count":9,"title":["Ordered Sets in the Calculus of Data Structures"],"prefix":"10.1007","author":[{"given":"Viktor","family":"Kuncak","sequence":"first","affiliation":[]},{"given":"Ruzica","family":"Piskac","sequence":"additional","affiliation":[]},{"given":"Philippe","family":"Suter","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"5","key":"5_CR1","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), http:\/\/dx.doi.org\/10.1016\/j.orl.2005.09.008","journal-title":"Operations Research Letters"},{"key":"5_CR2","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":"3-4","key":"5_CR3","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/s10817-004-6241-5","volume":"33","author":"S. Ghilardi","year":"2005","unstructured":"Ghilardi, S.: Model theoretic methods in combined constraint satisfiability. Journal of Automated Reasoning\u00a033(3-4), 221\u2013249 (2005)","journal-title":"Journal of Automated Reasoning"},{"key":"5_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1007\/978-3-540-27813-9_14","volume-title":"Computer Aided Verification","author":"H. Ganzinger","year":"2004","unstructured":"Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL(T): Fast decision procedures. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 175\u2013188. Springer, Heidelberg (2004)"},{"key":"5_CR5","doi-asserted-by":"crossref","unstructured":"Kuncak, V., Mayer, M., Piskac, R., Suter, P.: Complete functional synthesis. In: PLDI (2010)","DOI":"10.1145\/1806596.1806632"},{"key":"5_CR6","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":"5_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1007\/978-3-642-11319-2_6","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"V. Kuncak","year":"2010","unstructured":"Kuncak, V., Piskac, R., Suter, P., Wies, T.: Building a calculus of data structures. In: Barthe, G., Hermenegildo, M. (eds.) VMCAI 2010. LNCS, vol.\u00a05944, pp. 26\u201344. Springer, Heidelberg (2010)"},{"key":"5_CR8","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":"5_CR9","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1016\/S0049-237X(08)70525-1","volume":"50","author":"H. Laeuchli","year":"1968","unstructured":"Laeuchli, H.: A decision procedure for the weak second order theory of linear order. Studies in Logic and the Foundat. of Math.\u00a050, 189\u2013197 (1968)","journal-title":"Studies in Logic and the Foundat. of Math."},{"issue":"1","key":"5_CR10","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1145\/357084.357090","volume":"2","author":"Z. Manna","year":"1980","unstructured":"Manna, Z., Waldinger, R.: A deductive approach to program synthesis. ACM Trans. Program. Lang. Syst.\u00a02(1), 90\u2013121 (1980)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"5_CR11","unstructured":"Odersky, M., Spoon, L., Venners, B.: Programming in Scala: a comprehensive step-by-step guide. Artima Press (2008)"},{"issue":"3","key":"5_CR12","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":"5_CR13","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":"5_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1007\/978-3-540-87531-4_11","volume-title":"Computer Science Logic","author":"R. Piskac","year":"2008","unstructured":"Piskac, R., Kuncak, V.: Fractional collections with cardinality bounds. In: Kaminski, M., Martini, S. (eds.) CSL 2008. LNCS, vol.\u00a05213, pp. 124\u2013138. Springer, Heidelberg (2008)"},{"key":"5_CR15","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":"4","key":"5_CR16","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":"5_CR17","first-page":"1","volume":"141","author":"M.O. Rabin","year":"1969","unstructured":"Rabin, M.O.: Decidability of second-order theories and automata on infinite trees. Trans. Amer. Math. Soc.\u00a0141, 1\u201335 (1969)","journal-title":"Trans. Amer. Math. Soc."},{"key":"5_CR18","doi-asserted-by":"crossref","unstructured":"Ramsey, F.P.: On a problem of formal logic. Proc. London Math. Soc.\u00a0s2-30, 264\u2013286 (1930), doi:10.1112\/plms\/s2-30.1.264","DOI":"10.1112\/plms\/s2-30.1.264"},{"key":"5_CR19","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1007\/11559306_3","volume-title":"Frontiers of Combining Systems","author":"S. Ranise","year":"2005","unstructured":"Ranise, S., Ringeissen, C., Zarba, C.G.: Combining data structures with nonstably infinite theories using many-sorted logic. In: Gramlich, B. (ed.) FroCos 2005. LNCS (LNAI), vol.\u00a03717, pp. 48\u201364. Springer, Heidelberg (2005)"},{"key":"5_CR20","doi-asserted-by":"crossref","unstructured":"Suter, P., Dotta, M., Kuncak, V.: Decision procedures for algebraic data types with abstractions. In: POPL (2010)","DOI":"10.1145\/1706299.1706325"},{"issue":"3","key":"5_CR21","doi-asserted-by":"publisher","first-page":"379","DOI":"10.2307\/1971037","volume":"102","author":"S. Shelah","year":"1975","unstructured":"Shelah, S.: The monadic theory of order. The Annals of Mathematics of Mathematics\u00a0102(3), 379\u2013419 (1975)","journal-title":"The Annals of Mathematics of Mathematics"},{"key":"5_CR22","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/978-3-540-74621-8_3","volume-title":"Frontiers of Combining Systems","author":"V. Sofronie-Stokkermans","year":"2007","unstructured":"Sofronie-Stokkermans, V.: Hierarchical and modular reasoning in complex theories: The case of local theory extensions. In: Konev, B., Wolter, F. (eds.) FroCos 2007. LNCS (LNAI), vol.\u00a04720, pp. 47\u201371. Springer, Heidelberg (2007)"},{"issue":"1","key":"5_CR23","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/BF01691346","volume":"2","author":"J.W. Thatcher","year":"1968","unstructured":"Thatcher, J.W., Wright, J.B.: Generalized finite automata theory with an application to a decision problem of second-order logic. Mathematical Systems Theory\u00a02(1), 57\u201381 (1968)","journal-title":"Mathematical Systems Theory"},{"key":"5_CR24","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":"5_CR25","doi-asserted-by":"crossref","unstructured":"Wies, T., Piskac, R., Kuncak, V.: Combining theories with shared set operations. In: Frontiers in Combining Systems (2009)","DOI":"10.1007\/978-3-642-04222-5_23"},{"key":"5_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"380","DOI":"10.1007\/978-3-642-11319-2_27","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"K. Yessenov","year":"2010","unstructured":"Yessenov, K., Piskac, R., Kuncak, V.: Collections, cardinalities, and relations. In: Barthe, G., Hermenegildo, M. (eds.) VMCAI 2010. LNCS, vol.\u00a05944, pp. 380\u2013395. Springer, Heidelberg (2010)"}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-15205-4_5.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T03:02:36Z","timestamp":1606186956000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-15205-4_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642152047","9783642152054"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-15205-4_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}