{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T21:51:20Z","timestamp":1725573080534},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540252368"},{"type":"electronic","value":"9783540322757"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/978-3-540-32275-7_4","type":"book-chapter","created":{"date-parts":[[2010,12,20]],"date-time":"2010-12-20T21:14:41Z","timestamp":1292879681000},"page":"51-66","source":"Crossref","is-referenced-by-count":6,"title":["Combining Lists with Non-stably Infinite Theories"],"prefix":"10.1007","author":[{"given":"Pascal","family":"Fontaine","sequence":"first","affiliation":[]},{"given":"Silvio","family":"Ranise","sequence":"additional","affiliation":[]},{"given":"Calogero G.","family":"Zarba","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"2","key":"4_CR1","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1016\/S0890-5401(03)00020-8","volume":"183","author":"A. Armando","year":"2003","unstructured":"Armando, A., Ranise, S., Rusinowitch, M.: A rewriting approach to satisfiability procedures. Information and Computation\u00a0183(2), 140\u2013164 (2003)","journal-title":"Information and Computation"},{"key":"4_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"521","DOI":"10.1007\/3-540-36577-X_38","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Berezin","year":"2003","unstructured":"Berezin, S., Ganesh, V., Dill, D.L.: An Online Proof-Producing Decision Procedure for Mixed-Integer Linear Arithmetic. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 521\u2013536. Springer, Heidelberg (2003)"},{"key":"4_CR3","unstructured":"Bj\u00f8rner, N.S.: Integrating Decision Procedures for Temporal Verification. PhD thesis, Stanford University (1998)"},{"key":"4_CR4","unstructured":"Boyer, R.S., Moore, J.S.: A Computational Logic. ACM Monograph SERIES (1979)"},{"key":"4_CR5","doi-asserted-by":"crossref","unstructured":"de Moura, L., Rue\u00df, H., Shankar, N.: Justifying equality. In: PDPAR (2004)","DOI":"10.1016\/j.entcs.2004.06.068"},{"key":"4_CR6","volume-title":"Proc. of the International Conference on Software Engineering and Formal Methods (SEFM 2003)","author":"D. D\u00e9harbe","year":"2003","unstructured":"D\u00e9harbe, D., Ranise, S.: Light-Weight Theorem Proving for Debugging and Verifying Units of Code. In: Proc. of the International Conference on Software Engineering and Formal Methods (SEFM 2003), IEEE Computer Society Press, Los Alamitos (2003)"},{"key":"4_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/3-540-44585-4_22","volume-title":"Computer Aided Verification","author":"J.-C. Filli\u00e2tre","year":"2001","unstructured":"Filli\u00e2tre, J.-C., Owre, S., Rue\u00df, H., Shankar, N.: ICS: integrated canonizer and solver. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 246\u2013249. Springer, Heidelberg (2001)"},{"key":"4_CR8","doi-asserted-by":"crossref","unstructured":"Fontaine, P., Gribomont, P.: Combining non-stably infinite, non-first order theories. In: Ranise, S., Tinelli, C. (eds.) Pragmatics of Decision Procedures in Automated Reasoning (2004)","DOI":"10.1016\/j.entcs.2004.06.066"},{"key":"4_CR9","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"332","DOI":"10.1007\/3-540-45620-1_28","volume-title":"Automated Deduction - CADE-18","author":"H. Ganzinger","year":"2002","unstructured":"Ganzinger, H.: Shostak light. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol.\u00a02392, pp. 332\u2013346. Springer, Heidelberg (2002)"},{"key":"4_CR10","unstructured":"Kapur, D., Nie, X.: Reasoning about Numbers in Tecton. In: Proc. 8th Inl. Symp. Methodologies for Intelligent Systems, pp. 57\u201370 (1994)"},{"key":"4_CR11","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/978-1-4612-3658-0_9","volume-title":"Current Trends in Hardware Verification and Theorem Proving","author":"T.F. Melham","year":"1989","unstructured":"Melham, T.F.: Automating Recursive Type Definitions in Higher Order Logic. In: Current Trends in Hardware Verification and Theorem Proving. LNCS, pp. 341\u2013386. Springer, Heidelberg (1989)"},{"issue":"2","key":"4_CR12","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.: Simplifications by cooperating decision procedures. ACM Trans. on Programming Languages and Systems\u00a01(2), 245\u2013257 (1979)","journal-title":"ACM Trans. on Programming Languages and Systems"},{"issue":"2","key":"4_CR13","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1145\/322186.322198","volume":"27","author":"G. Nelson","year":"1980","unstructured":"Nelson, G., Oppen, D.C.: Fast decision procedures based on congruence closure. Journal of the Association for Computing Machinery\u00a027(2), 356\u2013364 (1980)","journal-title":"Journal of the Association for Computing Machinery"},{"issue":"3","key":"4_CR14","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1145\/322203.322204","volume":"27","author":"D.C. Oppen","year":"1980","unstructured":"Oppen, D.C.: Reasoning about recursively defined data structures. Journal of the ACM\u00a027(3), 403\u2013411 (1980)","journal-title":"Journal of the ACM"},{"key":"4_CR15","unstructured":"Owre, S., Shankar, N.: Abstract Datatypes in PVS. Technical Report CSL-93- 9R, SRI International (1997)"},{"key":"4_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1007\/3-540-58156-1_11","volume-title":"Automated Deduction - CADE-12","author":"L.C. Paulson","year":"1994","unstructured":"Paulson, L.C.: A fixedpoint approach to implementing (co)inductive definitions. In: Bundy, A. (ed.) CADE 1994. LNCS, vol.\u00a0814, pp. 148\u2013161. Springer, Heidelberg (1994)"},{"key":"4_CR17","doi-asserted-by":"crossref","unstructured":"Pugh, W.: The omega test: a fast integer programming algorithm for dependence analysis. Supercomputing, 4\u201313 (1991)","DOI":"10.1145\/125826.125848"},{"issue":"1","key":"4_CR18","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2422.322411","volume":"31","author":"R.E. Shostak","year":"1984","unstructured":"Shostak, R.E.: Deciding combination of theories. Journal of the Association for Computing Machinery\u00a031(1), 1\u201312 (1984)","journal-title":"Journal of the Association for Computing Machinery"},{"key":"4_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"500","DOI":"10.1007\/3-540-45657-0_40","volume-title":"Computer Aided Verification","author":"A. Stump","year":"2002","unstructured":"Stump, A., Barrett, C.W., Dill, D.L.: CVC: a cooperating validity checker. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 500\u2013504. Springer, Heidelberg (2002)"},{"key":"4_CR20","doi-asserted-by":"crossref","unstructured":"Tinelli, C., Zarba, C.G.: Combining non-stably infinite theories. Journal of Automated Reasoning (2004) (to appear)","DOI":"10.1007\/s10817-005-5204-9"},{"key":"4_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-46419-0_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P. Wolper","year":"2000","unstructured":"Wolper, P., Boigelot, B.: On the construction of automata from linear arithmetic constraints. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol.\u00a01785, pp. 1\u201319. Springer, Heidelberg (2000)"},{"key":"4_CR22","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"363","DOI":"10.1007\/3-540-45620-1_30","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, pp. 363\u2013376. Springer, Heidelberg (2002)"},{"key":"4_CR23","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/3-540-45988-X_9","volume-title":"Frontiers of Combining Systems","author":"C.G. Zarba","year":"2002","unstructured":"Zarba, C.G.: Combining sets with integers. In: Armando, A. (ed.) FroCos 2002. LNCS (LNAI), vol.\u00a02309, pp. 103\u2013116. Springer, Heidelberg (2002)"},{"key":"4_CR24","series-title":"Lecture Notes in Computer Science","first-page":"762","volume-title":"Verification: Theory and Practice","author":"C.G. Zarba","year":"2004","unstructured":"Zarba, C.G.: Combining sets with elements. In: Dershowitz, N. (ed.) Verification: Theory and Practice. LNCS, vol.\u00a02772, pp. 762\u2013782. Springer, Heidelberg (2004)"},{"key":"4_CR25","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1007\/978-3-540-25984-8_9","volume-title":"Automated Reasoning","author":"T. Zhang","year":"2004","unstructured":"Zhang, T., Sipma, H.B., Manna, Z.: Decision procedures for recursive data structures with integer constraints. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol.\u00a03097, pp. 152\u2013167. Springer, Heidelberg (2004)"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-32275-7_4.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,11,16]],"date-time":"2021-11-16T00:03:42Z","timestamp":1637021022000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-32275-7_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540252368","9783540322757"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-32275-7_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}