{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T02:05:19Z","timestamp":1784167519264,"version":"3.55.0"},"publisher-location":"Berlin, Heidelberg","reference-count":36,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642042218","type":"print"},{"value":"9783642042225","type":"electronic"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-04222-5_23","type":"book-chapter","created":{"date-parts":[[2009,9,16]],"date-time":"2009-09-16T12:42:11Z","timestamp":1253104931000},"page":"366-382","source":"Crossref","is-referenced-by-count":24,"title":["Combining Theories with Shared Set Operations"],"prefix":"10.1007","author":[{"given":"Thomas","family":"Wies","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ruzica","family":"Piskac","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Viktor","family":"Kuncak","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"23_CR1","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-015-9934-4","volume-title":"An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof","author":"P.B. Andrews","year":"2002","unstructured":"Andrews, P.B.: An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, 2nd edn. Springer (Kluwer), Heidelberg (2002)","edition":"2"},{"key":"23_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1007\/3-540-46002-0_12","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T. Ball","year":"2002","unstructured":"Ball, T., Podelski, A., Rajamani, S.K.: Relative completeness of abstraction refinement for software model checking. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol.\u00a02280, p. 158. Springer, Heidelberg (2002)"},{"issue":"6","key":"23_CR3","doi-asserted-by":"publisher","first-page":"27","DOI":"10.5381\/jot.2004.3.6.a2","volume":"3","author":"M. Barnett","year":"2004","unstructured":"Barnett, M., DeLine, R., F\u00e4hndrich, M., Leino, K.R.M., Schulte, W.: Verification of object-oriented programs with invariants. Journal of Object Technology\u00a03(6), 27\u201356 (2004)","journal-title":"Journal of Object Technology"},{"key":"23_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)"},{"key":"23_CR5","unstructured":"Basin, D., Friedrich, S.: Combining WS1S and HOL. In: FroCoS (1998)"},{"key":"23_CR6","doi-asserted-by":"publisher","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":"23_CR7","volume-title":"Machine Intelligence","author":"R.S. Boyer","year":"1988","unstructured":"Boyer, R.S., Moore, J.S.: Integrating decision procedures into heuristic theorem provers: A case study of linear arithmetic. In: Machine Intelligence, vol.\u00a011. Oxford University Press, Oxford (1988)"},{"key":"23_CR8","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.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"23_CR9","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"},{"key":"23_CR10","unstructured":"Fontaine, P.: Combinations of theories and the bernays-sch\u00f6nfinkel-ramsey class. In: VERIFY (2007)"},{"key":"23_CR11","series-title":"LNAI","first-page":"263","volume-title":"FroCoS 2009","author":"P. Fontaine","year":"2009","unstructured":"Fontaine, P.: Combinations of theories for decidable fragments of first-order logic. In: Ghilardi, S., Sebastiani, R. (eds.) FroCoS 2009. LNCS (LNAI), vol.\u00a05749, pp. 263\u2013278. Springer, Heidelberg (2009)"},{"key":"23_CR12","volume-title":"Principles of Knowledge Representation and Reasoning","author":"D.M. Gabbay","year":"1992","unstructured":"Gabbay, D.M., Ohlbach, H.J.: Quantifier elimination in second-order predicate logic. In: Nebel, B., Rich, C., Swartout, W. (eds.) Principles of Knowledge Representation and Reasoning. Morgan-Kaufmann, San Francisco (1992)"},{"key":"23_CR13","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":"3-4","key":"23_CR14","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"},{"issue":"2","key":"23_CR15","doi-asserted-by":"publisher","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":"23_CR16","doi-asserted-by":"crossref","unstructured":"Klaedtke, F., Rue\u00df, H.: Parikh automata and monadic second-order logics with linear cardinality constraints. Technical Report 177, Institute of Computer Science at Freiburg University (2002)","DOI":"10.1007\/3-540-45061-0_54"},{"key":"23_CR17","series-title":"Lecture Notes in Computer Science","volume-title":"Automata, Languages and Programming","author":"F. Klaedtke","year":"2003","unstructured":"Klaedtke, F., Rue\u00df, H.: Monadic second-order logics with cardinalities. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) ICALP 2003. LNCS, vol.\u00a02719. Springer, Heidelberg (2003)"},{"key":"23_CR18","unstructured":"Klarlund, N., M\u00f8ller, A.: MONA Version 1.4 User Manual. BRICS Notes Series NS-01-1, Department of Computer Science. University of Aarhus (January 2001)"},{"key":"23_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"602","DOI":"10.1007\/978-3-540-71209-1_47","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Krstic","year":"2007","unstructured":"Krstic, S., Goel, A., Grundy, J., Tinelli, C.: Combined satisfiability modulo parametric theories. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 602\u2013617. Springer, Heidelberg (2007)"},{"key":"23_CR20","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":"23_CR21","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":"23_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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)"},{"key":"23_CR23","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"},{"issue":"2","key":"23_CR24","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":"23_CR25","doi-asserted-by":"crossref","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: A prototype verification system. In: Kapur, D. (ed.) 11th CADE, June 1992. LNCS (LNAI), vol.\u00a0607, pp. 748\u2013752 (1992)","DOI":"10.1007\/3-540-55602-8_217"},{"issue":"4","key":"23_CR26","doi-asserted-by":"publisher","first-page":"570","DOI":"10.1145\/321356.321364","volume":"13","author":"R.J. Parikh","year":"1966","unstructured":"Parikh, R.J.: On context-free languages. J. ACM\u00a013(4), 570\u2013581 (1966)","journal-title":"J. ACM"},{"key":"23_CR27","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":"23_CR28","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":"3","key":"23_CR29","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":"23_CR30","doi-asserted-by":"publisher","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.\u00a0s2-30, 264\u2013286 (1930), doi:10.1112\/plms\/s2-30.1.264","journal-title":"Proc. London Math. Soc."},{"issue":"1","key":"23_CR31","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"},{"issue":"1","key":"23_CR32","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1016\/S0304-3975(01)00332-2","volume":"290","author":"C. Tinelli","year":"2003","unstructured":"Tinelli, C., Ringeissen, C.: Unions of non-disjoint theories and combinations of satisfiability procedures. Th. Comp. Sc.\u00a0290(1), 291\u2013353 (2003)","journal-title":"Th. Comp. Sc."},{"key":"23_CR33","doi-asserted-by":"crossref","unstructured":"Tinelli, C., Zarba, C.: Combining nonstably infinite theories. Journal of Automated Reasoning\u00a034(3) (2005)","DOI":"10.1007\/s10817-005-5204-9"},{"key":"23_CR34","unstructured":"Wies, T.: Symbolic Shape Analysis. PhD thesis. University of Freiburg (2009)"},{"key":"23_CR35","doi-asserted-by":"crossref","unstructured":"Wies, T., Piskac, R., Kuncak, V.: On Combining Theories with Shared Set Operations. Technical Report LARA-REPORT-2009-002, EPFL (May 2009)","DOI":"10.1007\/978-3-642-04222-5_23"},{"key":"23_CR36","doi-asserted-by":"crossref","unstructured":"Zee, K., Kuncak, V., Rinard, M.: Full functional verification of linked data structures. In: ACM Conf. Programming Language Design and Implementation, PLDI (2008)","DOI":"10.1145\/1375581.1375624"}],"container-title":["Lecture Notes in Computer Science","Frontiers of Combining Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-04222-5_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,22]],"date-time":"2019-05-22T13:17:36Z","timestamp":1558531056000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-04222-5_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642042218","9783642042225"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-04222-5_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009]]}}}