{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,28]],"date-time":"2025-11-28T04:47:12Z","timestamp":1764305232746},"publisher-location":"Berlin, Heidelberg","reference-count":36,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642221187"},{"type":"electronic","value":"9783642221194"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-22119-4_1","type":"book-chapter","created":{"date-parts":[[2011,6,15]],"date-time":"2011-06-15T14:21:08Z","timestamp":1308147668000},"page":"1-16","source":"Crossref","is-referenced-by-count":6,"title":["On Interpolation in Decision Procedures"],"prefix":"10.1007","author":[{"given":"Maria Paola","family":"Bonacina","sequence":"first","affiliation":[]},{"given":"Moa","family":"Johansson","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"1_CR1","first-page":"1","volume-title":"Proc. of the 12th Int. Symp. on Principles and Practice of Declarative Programming","author":"M.P. Bonacina","year":"2010","unstructured":"Bonacina, M.P.: On theorem proving for program checking \u2013 Historical perspective and recent developments. In: Fernandez, M. (ed.) Proc. of the 12th Int. Symp. on Principles and Practice of Declarative Programming, pp. 1\u201311. ACM Press, New York (2010)"},{"issue":"1","key":"1_CR2","doi-asserted-by":"publisher","first-page":"180","DOI":"10.1145\/1182613.1182619","volume":"8","author":"M.P. Bonacina","year":"2007","unstructured":"Bonacina, M.P., Dershowitz, N.: Abstract canonical inference. ACM Trans. on Computational Logic\u00a08(1), 180\u2013208 (2007)","journal-title":"ACM Trans. on Computational Logic"},{"key":"1_CR3","unstructured":"Bonacina, M.P., Johansson, M.: On theorem proving with interpolation for program checking. In: Technical report, Dipartimento di Informatica. Universit\u00e0 degli Studi di Verona (April 2011)"},{"key":"1_CR4","doi-asserted-by":"crossref","unstructured":"Bonacina, M.P., Lynch, C.A., de Moura, L.: On deciding satisfiability by theorem proving with speculative inferences. Journal of Automated Reasoning, 1\u201329 (in press); (Published online December 22, 2010) doi:10.1007\/s10817-010-9213-y","DOI":"10.1007\/s10817-010-9213-y"},{"volume-title":"The Calculus of Computation \u2013 Decision Procedures with Applications to Verification","year":"2007","key":"1_CR5","unstructured":"Bradley, A.R., Manna, Z. (eds.): The Calculus of Computation \u2013 Decision Procedures with Applications to Verification. Springer, Heidelberg (2007)"},{"key":"1_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"384","DOI":"10.1007\/978-3-642-14203-1_33","volume-title":"Automated Reasoning","author":"A. Brillout","year":"2010","unstructured":"Brillout, A., Kroening, D., R\u00fcmmer, P., Wahl, T.: An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS, vol.\u00a06173, pp. 384\u2013399. Springer, Heidelberg (2010)"},{"key":"1_CR7","unstructured":"Brillout, A., Kroening, D., R\u00fcmmer, P., Wahl, T.: Program verification via Craig interpolation for Presburger arithmetic with arrays. Notes of the 6th Int. Verification Workshop (2010), http:\/\/www.philipp.ruemmer.org\/"},{"key":"1_CR8","doi-asserted-by":"crossref","unstructured":"Bruttomesso, R., Ghilardi, S., Ranise, S.: Rewriting-based quantifier-free interpolation for a theory of arrays. In: Proc. of the 22nd Int. Conf. on Rewriting Techniques and Applications, LIPICS. Leibniz-Zentrum f\u00fcr Informatik, Dagsthul Publishing (2011)","DOI":"10.2168\/LMCS-8(2:4)2012"},{"key":"1_CR9","first-page":"770","volume-title":"Proc. of the 14th Int. Conf. on Computer-Aided Design","author":"R. Bruttomesso","year":"2010","unstructured":"Bruttomesso, R., Rollini, S., Sharygina, N., Tsitovich, A.: Flexible interpolation generation in satisfiability modulo theories. In: Proc. of the 14th Int. Conf. on Computer-Aided Design, pp. 770\u2013777. IEEE Computer Society Press, Los Alamitos (2010)"},{"issue":"5-6","key":"1_CR10","doi-asserted-by":"publisher","first-page":"705","DOI":"10.1016\/S0747-7171(06)80010-6","volume":"15","author":"R. Chadha","year":"1993","unstructured":"Chadha, R., Plaisted, D.A.: On the mechanical derivation of loop invariants. Journal of Symbolic Computation\u00a015(5-6), 705\u2013744 (1993)","journal-title":"Journal of Symbolic Computation"},{"key":"1_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1007\/978-3-540-78800-3_30","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Cimatti","year":"2008","unstructured":"Cimatti, A., Griggio, A., Sebastiani, R.: Efficient Interpolant Generation in Satisfiability Modulo Theories. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 397\u2013412. Springer, Heidelberg (2008)"},{"key":"1_CR12","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-642-02959-2_15","volume-title":"Automated Deduction \u2013 CADE-22","author":"A. Cimatti","year":"2009","unstructured":"Cimatti, A., Griggio, A., Sebastiani, R.: Interpolant Generation for UTVPI. In: Schmidt, R. (ed.) CADE-22. LNCS (LNAI), vol.\u00a05663, pp. 167\u2013182. Springer, Heidelberg (2009)"},{"key":"1_CR13","doi-asserted-by":"crossref","unstructured":"de Moura, L., Bj\u00f8rner, N.: Model-based theory combination. In: Krsti\u0107, S., Oliveras, A. (eds.) CAV 2007. ENTCS, vol.\u00a0198(2), pp. 37\u201349. Elsevier, Amsterdam (2008)","DOI":"10.1016\/j.entcs.2008.04.079"},{"key":"1_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/978-3-642-11957-6_11","volume-title":"Programming Languages and Systems","author":"V. D\u2019Silva","year":"2010","unstructured":"D\u2019Silva, V.: Propositional Interpolation and Abstract Interpretation. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol.\u00a06012, pp. 185\u2013204. Springer, Heidelberg (2010)"},{"key":"1_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/978-3-642-11319-2_12","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"V. D\u2019Silva","year":"2010","unstructured":"D\u2019Silva, V., Kroening, D., Purandare, M., Weissenbacher, G.: Interpolant Strength. In: Barthe, G., Hermenegildo, M. (eds.) VMCAI 2010. LNCS, vol.\u00a05944, pp. 129\u2013145. Springer, Heidelberg (2010)"},{"key":"1_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1007\/978-3-642-00768-2_34","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Fuchs","year":"2009","unstructured":"Fuchs, A., Goel, A., Grundy, J., Krsti\u0107, S., Tinelli, C.: Ground Interpolation for the Theory of Equality. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol.\u00a05505, pp. 413\u2013427. Springer, Heidelberg (2009)"},{"key":"1_CR17","doi-asserted-by":"crossref","unstructured":"Goel, A., Krsti\u0107, S., Tinelli, C.: Ground Interpolation for Combined Theories. In: Schmidt, R. (ed.) CADE-22. LNCS, vol.\u00a05663, pp. 183\u2013198. Springer, Heidelberg (2009)","DOI":"10.1007\/978-3-642-02959-2_16"},{"key":"1_CR18","first-page":"232","volume-title":"Proc. of the 31st ACM SIGACT-SIGPLAN Symp. on Principles of Programming Languages","author":"T.A. Henzinger","year":"2004","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: Leroy, X. (ed.) Proc. of the 31st ACM SIGACT-SIGPLAN Symp. on Principles of Programming Languages, pp. 232\u2013244. ACM Press, New York (2004)"},{"key":"1_CR19","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/978-3-642-14203-1_16","volume-title":"Automated Reasoning","author":"K. Hoder","year":"2010","unstructured":"Hoder, K., Kov\u00e1cs, L., Voronkov, A.: Interpolation and Symbol Elimination in Vampire. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS (LNAI), vol.\u00a06173, pp. 188\u2013195. Springer, Heidelberg (2010)"},{"key":"1_CR20","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/BFb0030832","volume-title":"Proc. of the 1st Annual Int. Conf. on Computing and Combinatorics","author":"G. Huang","year":"1995","unstructured":"Huang, G.: Constructing Craig interpolation formulas. In: Proc. of the 1st Annual Int. Conf. on Computing and Combinatorics, pp. 181\u2013190. Springer, Heidelberg (1995)"},{"key":"1_CR21","volume-title":"Proc. of the 14th ACM SIGSOFT Symp. on the Foundations of Software Engineering","author":"D. Kapur","year":"2006","unstructured":"Kapur, D., Majumdar, R., Zarba, C.G.: Interpolation for data structures. In: Devambu, P. (ed.) Proc. of the 14th ACM SIGSOFT Symp. on the Foundations of Software Engineering, ACM Press, New York (2006)"},{"key":"1_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"470","DOI":"10.1007\/978-3-642-00593-0_33","volume-title":"Fundamental Approaches to Software Engineering","author":"L. Kov\u00e1cs","year":"2009","unstructured":"Kov\u00e1cs, L., Voronkov, A.: Finding loop invariants for programs over arrays using a theorem prover. In: Chechik, M., Wirsing, M. (eds.) FASE 2009. LNCS, vol.\u00a05503, pp. 470\u2013485. Springer, Heidelberg (2009)"},{"key":"1_CR23","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/978-3-642-02959-2_17","volume-title":"Automated Deduction \u2013 CADE-22","author":"L. Kov\u00e1cs","year":"2009","unstructured":"Kov\u00e1cs, L., Voronkov, A.: Interpolation and Symbol Elimination. In: Schmidt, R. (ed.) CADE-22. LNCS (LNAI), vol.\u00a05663, pp. 199\u2013213. Springer, Heidelberg (2009)"},{"issue":"2","key":"1_CR24","doi-asserted-by":"publisher","first-page":"457","DOI":"10.2307\/2275541","volume":"62","author":"J. Kraj\u00ed\u010dek","year":"1997","unstructured":"Kraj\u00ed\u010dek, J.: Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic. Journal of Symbolic Logic\u00a062(2), 457\u2013486 (1997)","journal-title":"Journal of Symbolic Logic"},{"key":"1_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-45069-6_1","volume-title":"Computer Aided Verification","author":"K.L. McMillan","year":"2003","unstructured":"McMillan, K.L.: Interpolation and SAT-Based Model Checking. In: Hunt, W.J., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 1\u201313. Springer, Heidelberg (2003)"},{"issue":"1","key":"1_CR26","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. Theoretical Computer Science\u00a0345(1), 101\u2013121 (2005)","journal-title":"Theoretical Computer Science"},{"key":"1_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1007\/978-3-540-78800-3_31","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K.L. McMillan","year":"2008","unstructured":"McMillan, K.L.: Quantified Invariant Generation Using an Interpolating Saturation Prover. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 413\u2013427. Springer, Heidelberg (2008)"},{"key":"1_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"104","DOI":"10.1007\/978-3-642-14295-6_10","volume-title":"Computer Aided Verification","author":"K.L. McMillan","year":"2010","unstructured":"McMillan, K.L.: Lazy Annotation for Program Testing and Verification. In: Cook, B., Jackson, P., Touili, T. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 104\u2013118. Springer, Heidelberg (2010)"},{"issue":"2","key":"1_CR29","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 Trans. on Programming Languages and Systems\u00a01(2), 245\u2013257 (1979)","journal-title":"ACM Trans. on Programming Languages and Systems"},{"issue":"2","key":"1_CR30","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 ACM\u00a027(2), 356\u2013364 (1980)","journal-title":"Journal of the ACM"},{"issue":"6","key":"1_CR31","doi-asserted-by":"publisher","first-page":"937","DOI":"10.1145\/1217856.1217859","volume":"53","author":"R. Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: From an abstract Davis\u2013Putnam\u2013Logemann\u2013Loveland procedure to DPLL(T). Journal of the ACM\u00a053(6), 937\u2013977 (2006)","journal-title":"Journal of the ACM"},{"issue":"3","key":"1_CR32","doi-asserted-by":"publisher","first-page":"981","DOI":"10.2307\/2275583","volume":"62","author":"P. Pudl\u00e0k","year":"1997","unstructured":"Pudl\u00e0k, P.: Lower bounds for resolution and cutting plane proofs and monotone computations. Journal of Symbolic Logic\u00a062(3), 981\u2013998 (1997)","journal-title":"Journal of Symbolic Logic"},{"key":"1_CR33","doi-asserted-by":"crossref","first-page":"141","DOI":"10.3233\/SAT190034","volume":"3","author":"R. Sebastiani","year":"2006","unstructured":"Sebastiani, R.: Lazy satisfiability modulo theory. Journal on Satisfiability, Boolean Modelling and Computation\u00a03, 141\u2013224 (2006)","journal-title":"Journal on Satisfiability, Boolean Modelling and Computation"},{"issue":"4","key":"1_CR34","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1145\/1592434.1592437","volume":"41","author":"N. Shankar","year":"2009","unstructured":"Shankar, N.: Automated deduction for verification. ACM Computing Surveys\u00a041(4), 40\u201396 (2009)","journal-title":"ACM Computing Surveys"},{"key":"1_CR35","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","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.) CADE 2005. LNCS (LNAI), vol.\u00a03632, pp. 353\u2013368. Springer, Heidelberg (2005); Early version in MSR-TR-2004-108 (October 2004)"},{"key":"1_CR36","first-page":"10880","volume-title":"Proc. of the Conf. on Design Automation and Test in Europe","author":"L. Zhang","year":"2003","unstructured":"Zhang, L., Malik, S.: Validating SAT solvers using an independent resolution-based checker: practical implementations and other applications. In: Proc. of the Conf. on Design Automation and Test in Europe, pp. 10880\u201310885. IEEE Computer Society Press, Los Alamitos (2003)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-22119-4_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,6,20]],"date-time":"2020-06-20T04:55:56Z","timestamp":1592628956000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-22119-4_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642221187","9783642221194"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-22119-4_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}