{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T00:00:15Z","timestamp":1725494415730},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540697350"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-69738-1_25","type":"book-chapter","created":{"date-parts":[[2007,11,12]],"date-time":"2007-11-12T07:58:07Z","timestamp":1194854287000},"page":"346-362","source":"Crossref","is-referenced-by-count":48,"title":["Constraint Solving for Interpolation"],"prefix":"10.1007","author":[{"given":"Andrey","family":"Rybalchenko","sequence":"first","affiliation":[]},{"given":"Viorica","family":"Sofronie-Stokkermans","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"25_CR1","first-page":"196","volume-title":"PLDI\u20192003: Programming Language Design and Implementation","author":"B. Blanchet","year":"2003","unstructured":"Blanchet, B., et al.: A static analyzer for large safety-critical software. In: PLDI\u20192003: Programming Language Design and Implementation, 7\u201314, pp. 196\u2013207. ACM Press, New York (2003)"},{"key":"25_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"491","DOI":"10.1007\/11513988_48","volume-title":"Computer Aided Verification","author":"A.R. Bradley","year":"2005","unstructured":"Bradley, A.R., Manna, Z., Sipma, H.B.: Linear ranking with reachability. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 491\u2013504. Springer, Heidelberg (2005)"},{"key":"25_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"420","DOI":"10.1007\/978-3-540-45069-6_39","volume-title":"Computer Aided Verification","author":"M. Col\u00f3n","year":"2003","unstructured":"Col\u00f3n, M., Sankaranarayanan, S., Sipma, H.: Linear invariant generation using non-linear constraint solving. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 420\u2013432. Springer, Heidelberg (2003)"},{"key":"25_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/b105073","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"P. Cousot","year":"2005","unstructured":"Cousot, P.: Proving program invariance and termination by parametric abstraction, lagrangian relaxation and semidefinite programming. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 1\u201324. Springer, Heidelberg (2005)"},{"issue":"3","key":"25_CR5","doi-asserted-by":"publisher","first-page":"250","DOI":"10.2307\/2963593","volume":"22","author":"W. Craig","year":"1957","unstructured":"Craig, W.: Linear reasoning. A new form of the Herbrand-Gentzen theorem. J. Symb. Log.\u00a022(3), 250\u2013268 (1957)","journal-title":"J. Symb. Log."},{"key":"25_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"489","DOI":"10.1007\/11691372_35","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J. Esparza","year":"2006","unstructured":"Esparza, J., Kiefer, S., Schwoon, S.: Abstraction refinement with Craig interpolation and symbolic pushdown systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006 and ETAPS 2006. LNCS, vol.\u00a03920, pp. 489\u2013503. Springer, Heidelberg (2006)"},{"key":"25_CR7","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1145\/964001.964021","volume-title":"POPL: Principles of Programming Languages","author":"T.A. Henzinger","year":"2004","unstructured":"Henzinger, T.A., et al.: Abstractions from proofs. In: POPL: Principles of Programming Languages, pp. 232\u2013244. ACM Press, New York (2004)"},{"key":"25_CR8","unstructured":"Holzbaur, C.: OFAI clp(q,r) Manual, Edition 1.3.3. Austrian Research Institute for Artificial Intelligence, Vienna. TR-95-09 (1995)"},{"key":"25_CR9","volume-title":"ICLP 1987: Int. Conf. on Logic Programming, vol. 1","author":"J. Jaffar","year":"1987","unstructured":"Jaffar, J., Michaylov, S.: Methodology and implementation of a CLP system. In: ICLP 1987: Int. Conf. on Logic Programming, vol. 1, MIT Press, Cambridge (1987)"},{"key":"25_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1007\/11513988_6","volume-title":"Computer Aided Verification","author":"R. Jhala","year":"2005","unstructured":"Jhala, R., McMillan, K.L.: Interpolant-based transition relation approximation. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 39\u201351. Springer, Heidelberg (2005)"},{"key":"25_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"459","DOI":"10.1007\/11691372_33","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R. Jhala","year":"2006","unstructured":"Jhala, R., McMillan, K.L.: A practical and complete approach to predicate refinement. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006 and ETAPS 2006. LNCS, vol.\u00a03920, pp. 459\u2013473. Springer, Heidelberg (2006)"},{"key":"25_CR12","series-title":"Lecture Notes in Computer Science","volume-title":"Fast Software Encryption","author":"D. Kapur","year":"2006","unstructured":"Kapur, D., Majumdar, R., Zarba, C.G.: Interpolation for data structures. In: Robshaw, M. (ed.) FSE 2006. LNCS, vol.\u00a04047, Springer, Heidelberg (2006)"},{"issue":"1-2","key":"25_CR13","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1016\/S0304-3975(00)00177-8","volume":"266","author":"M. Koubarakis","year":"2001","unstructured":"Koubarakis, M.: Tractable disjunctions of linear constraints: Basic results and applications to temporal reasoning. Theoretical Computer Science\u00a0266(1-2), 311\u2013339 (2001)","journal-title":"Theoretical Computer Science"},{"issue":"2","key":"25_CR14","doi-asserted-by":"publisher","first-page":"457","DOI":"10.2307\/2275541","volume":"62","author":"J. Kraj\u00edcek","year":"1997","unstructured":"Kraj\u00edcek, J.: Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic. J. Symb. Log.\u00a062(2), 457\u2013486 (1997)","journal-title":"J. Symb. Log."},{"key":"25_CR15","unstructured":"T.I.S. Laboratory SICStus Prolog User\u2019s Manual. Swedish Institute of Computer Science, PO Box 1263 SE-164 29 Kista, Sweden. Release 3.8.7 (October 2001)"},{"key":"25_CR16","series-title":"Lecture Notes in Computer Science","first-page":"1","volume-title":"Computer Aided Verification","author":"K.L. McMillan","year":"2003","unstructured":"McMillan, K.L.: Interpolation and SAT-based model checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 1\u201313. Springer, Heidelberg (2003)"},{"issue":"1","key":"25_CR17","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/j.tcs.2005.07.003","volume":"345","author":"K.L. McMillan","year":"2005","unstructured":"McMillan, K.L.: An interpolating theorem prover. Theor. Comput. Sci.\u00a0345(1), 101\u2013121 (2005)","journal-title":"Theor. Comput. Sci."},{"key":"25_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/11817963_14","volume-title":"Computer Aided Verification","author":"K.L. McMillan","year":"2006","unstructured":"McMillan, K.L.: Lazy abstraction with interpolants. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 123\u2013136. Springer, Heidelberg (2006)"},{"key":"25_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"332","DOI":"10.1007\/11921240_23","volume-title":"Theoretical Aspects of Computing - ICTAC 2006","author":"R. Meyer","year":"2006","unstructured":"Meyer, R., Faber, J., Rybalchenko, A.: Model checking duration calculus: A practical approach. In: Barkaoui, K., Cavalcanti, A., Cerone, A. (eds.) ICTAC 2006. LNCS, vol.\u00a04281, pp. 332\u2013346. Springer, Heidelberg (2006)"},{"key":"25_CR20","series-title":"Lecture Notes in Computer Science","volume-title":"Practical Aspects of Declarative Languages","author":"A. Podelski","year":"2006","unstructured":"Podelski, A., Rybalchenko, A.: ARMC: the logical choice for software model checking with abstraction refinement. In: Hanus, M. (ed.) PADL 2007. LNCS, vol.\u00a04354, Springer, Heidelberg (2006)"},{"issue":"3","key":"25_CR21","doi-asserted-by":"publisher","first-page":"981","DOI":"10.2307\/2275583","volume":"62","author":"P. Pudl\u00e1k","year":"1997","unstructured":"Pudl\u00e1k, P.: Lower bounds for resolution and cutting plane proofs and monotone computations. J. Symb. Log.\u00a062(3), 981\u2013998 (1997)","journal-title":"J. Symb. Log."},{"key":"25_CR22","volume-title":"Theory of Linear and Integer Programming","author":"A. Schrijver","year":"1986","unstructured":"Schrijver, A.: Theory of Linear and Integer Programming. John Wiley & Sons, Chichester (1986)"},{"key":"25_CR23","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"219","DOI":"10.1007\/11532231_16","volume-title":"Automated Deduction \u2013 CADE-20","author":"V. Sofronie-Stokkermans","year":"2005","unstructured":"Sofronie-Stokkermans, V.: Hierarchic reasoning in local theory extensions. In: Nieuwenhuis, R. (ed.) Automated Deduction \u2013 CADE-20. LNCS (LNAI), vol.\u00a03632, pp. 219\u2013234. Springer, Heidelberg (2005)"},{"key":"25_CR24","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/11814771_21","volume-title":"Automated Reasoning","author":"V. Sofronie-Stokkermans","year":"2006","unstructured":"Sofronie-Stokkermans, V.: Interpolation in local theory extensions. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 235\u2013250. Springer, Heidelberg (2006)"},{"issue":"3","key":"25_CR25","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1016\/0020-0190(85)90076-6","volume":"20","author":"E. Sontag","year":"1985","unstructured":"Sontag, E.: Real addition and the polynomial hierarchy. Information Processing Letters\u00a020(3), 115\u2013120 (1985)","journal-title":"Information Processing Letters"},{"key":"25_CR26","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1007\/11532231_26","volume-title":"Automated Deduction \u2013 CADE-20","author":"G. Yorsh","year":"2005","unstructured":"Yorsh, G., Musuvathi, M.: A combination method for generating interpolants. In: Nieuwenhuis, R. (ed.) Automated Deduction \u2013 CADE-20. LNCS (LNAI), vol.\u00a03632, pp. 353\u2013368. Springer, Heidelberg (2005)"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-69738-1_25.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,3]],"date-time":"2021-05-03T00:45:09Z","timestamp":1620002709000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-69738-1_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540697350"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-69738-1_25","relation":{},"subject":[]}}