{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T13:29:27Z","timestamp":1725542967345},"publisher-location":"Berlin, Heidelberg","reference-count":33,"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_6","type":"book-chapter","created":{"date-parts":[[2010,1,6]],"date-time":"2010-01-06T05:00:05Z","timestamp":1262754005000},"page":"26-44","source":"Crossref","is-referenced-by-count":15,"title":["Building a Calculus of Data Structures"],"prefix":"10.1007","author":[{"given":"Viktor","family":"Kuncak","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ruzica","family":"Piskac","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Philippe","family":"Suter","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Wies","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"6_CR1","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-59207-2","volume-title":"The Classical Decision Problem","author":"E. B\u00f6rger","year":"1997","unstructured":"B\u00f6rger, E., Gr\u00e4del, E., Gurevich, Y.: The Classical Decision Problem. Springer, Heidelberg (1997)"},{"key":"6_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)"},{"issue":"8","key":"6_CR3","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1016\/j.entcs.2006.11.037","volume":"174","author":"C. Barrett","year":"2007","unstructured":"Barrett, C., Shikanian, I., Tinelli, C.: An abstract decision procedure for satisfiability in the theory of recursive data types. Electronic Notes in Theoretical Computer Science\u00a0174(8), 23\u201337 (2007)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"6_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/978-3-540-73368-3_34","volume-title":"Computer Aided Verification","author":"C. Barrett","year":"2007","unstructured":"Barrett, C., Tinelli, C.: CVC3. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 298\u2013302. Springer, Heidelberg (2007)"},{"issue":"2","key":"6_CR5","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1006\/inco.1994.1056","volume":"112","author":"H. Comon","year":"1994","unstructured":"Comon, H., Delor, C.: Equational formulae with membership constraints. Information and Computation\u00a0112(2), 167\u2013216 (1994)","journal-title":"Information and Computation"},{"key":"6_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.S.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"6_CR7","doi-asserted-by":"crossref","unstructured":"de Moura, L., Bj\u00f8rner, N.: Generalized, efficient array decision procedures. In: FMCAD (2009)","DOI":"10.1109\/FMCAD.2009.5351142"},{"issue":"5","key":"6_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":"6_CR9","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)"},{"key":"6_CR10","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)"},{"issue":"2","key":"6_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, Presburger formulas and languages. Pacific Journal of Mathematics\u00a016(2), 285\u2013296 (1966)","journal-title":"Pacific Journal of Mathematics"},{"key":"6_CR12","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":"6_CR13","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":"6_CR14","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":"2","key":"6_CR15","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G. Nelson","year":"1979","unstructured":"Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM TOPLAS\u00a01(2), 245\u2013257 (1979)","journal-title":"ACM TOPLAS"},{"key":"6_CR16","doi-asserted-by":"crossref","unstructured":"Oppen, D.C.: Reasoning about recursively defined data structures. In: POPL, pp. 151\u2013157 (1978)","DOI":"10.1145\/512760.512776"},{"key":"6_CR17","unstructured":"Odersky, M., Spoon, L., Venners, B.: Programming in Scala: a comprehensive step-by-step guide. Artima Press (2008)"},{"issue":"4","key":"6_CR18","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"},{"issue":"3","key":"6_CR19","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":"6_CR20","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":"6_CR21","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":"6_CR22","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)"},{"key":"6_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":"6_CR24","unstructured":"Presburger, M.: \u00dcber die Vollst\u00e4ndigkeit eines gewissen Systems der Aritmethik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. In: Comptes Rendus du premier Congr\u00e8s des Math\u00e9maticiens des Pays slaves, Warsawa, pp. 92\u2013101 (1929)"},{"issue":"4","key":"6_CR25","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":"6_CR26","doi-asserted-by":"crossref","first-page":"264","DOI":"10.1112\/plms\/s2-30.1.264","volume":"s2-30","author":"F.P. Ramsey","year":"1930","unstructured":"Ramsey, F.P.: On a problem of formal logic. Proc. London Math. Soc., s2-30, 264\u2013286 (1930)","journal-title":"Proc. London Math. Soc."},{"key":"6_CR27","doi-asserted-by":"crossref","unstructured":"Stump, A., Barrett, C.W., Dill, D.L., Levitt, J.R.: A decision procedure for an extensional theory of arrays. In: LICS, pp. 29\u201337 (2001)","DOI":"10.1109\/LICS.2001.932480"},{"key":"6_CR28","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"},{"key":"6_CR29","unstructured":"Skolem, T.: Untersuchungen \u00fcber die Axiome des Klassenkalk\u00fcls und \u00fcber Produktations- und Summationsprobleme, welche gewisse Klassen von Aussagen betreffen. Skrifter utgit av Vidnskapsselskapet i Kristiania, I. klasse, no. 3, Oslo (1919)"},{"issue":"1","key":"6_CR30","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":"6_CR31","unstructured":"Wies, T.: Symbolic Shape Analysis. PhD thesis, University of Freiburg (2009)"},{"key":"6_CR32","doi-asserted-by":"crossref","unstructured":"Wies, T., Piskac, R., Kuncak, V.: Combining theories with shared set operations. In: FroCoS: Frontiers in Combining Systems (2009)","DOI":"10.1007\/978-3-642-04222-5_23"},{"key":"6_CR33","doi-asserted-by":"crossref","unstructured":"Zee, K., Kuncak, V., Rinard, M.: Full functional verification of linked data structures. In: 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_6.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T02:39:32Z","timestamp":1606185572000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-11319-2_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642113185","9783642113192"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-11319-2_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}