{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,7]],"date-time":"2025-11-07T09:20:25Z","timestamp":1762507225138},"publisher-location":"Cham","reference-count":25,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319703886"},{"type":"electronic","value":"9783319703893"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-70389-3_13","type":"book-chapter","created":{"date-parts":[[2017,11,11]],"date-time":"2017-11-11T09:42:30Z","timestamp":1510393350000},"page":"195-210","source":"Crossref","is-referenced-by-count":8,"title":["LRA Interpolants from No Man\u2019s Land"],"prefix":"10.1007","author":[{"given":"Leonardo","family":"Alt","sequence":"first","affiliation":[]},{"given":"Antti E. J.","family":"Hyv\u00e4rinen","sequence":"additional","affiliation":[]},{"given":"Natasha","family":"Sharygina","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,11,12]]},"reference":[{"key":"13_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1007\/978-3-642-39799-8_22","volume-title":"Computer Aided Verification","author":"A Albarghouthi","year":"2013","unstructured":"Albarghouthi, A., McMillan, K.L.: Beautiful interpolants. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 313\u2013329. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_22"},{"key":"13_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/978-3-662-54580-5_12","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Alt","year":"2017","unstructured":"Alt, L., Asadi, S., Chockler, H., Even Mendoza, K., Fedyukovich, G., Hyv\u00e4rinen, A.E.J., Sharygina, N.: HiFrog: SMT-based function summarization for software verification. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10206, pp. 207\u2013213. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54580-5_12"},{"key":"13_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-319-29613-5_1","volume-title":"Verified Software: Theories, Tools, and Experiments","author":"L Alt","year":"2016","unstructured":"Alt, L., Fedyukovich, G., Hyv\u00e4rinen, A.E.J., Sharygina, N.: A proof-sensitive approach for small propositional interpolants. In: Gurfinkel, A., Seshia, S.A. (eds.) VSTTE 2015. LNCS, vol. 9593, pp. 1\u201318. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-29613-5_1"},{"key":"13_CR4","doi-asserted-by":"crossref","unstructured":"Alt, L., Hyv\u00e4rinen, A.E.J., Asadi, S., Sharygina, N.: Duality-based interpolation for quantifier-free equalities and uninterpreted functions. In: Proc. FMCAD (2017) (to appear)","DOI":"10.23919\/FMCAD.2017.8102239"},{"key":"13_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"589","DOI":"10.1007\/978-3-662-54577-5_34","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Bogomolov","year":"2017","unstructured":"Bogomolov, S., Frehse, G., Giacobbe, M., Henzinger, T.A.: Counterexample-guided refinement of template polyhedra. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 589\u2013606. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54577-5_34"},{"issue":"3","key":"13_CR6","doi-asserted-by":"crossref","first-page":"269","DOI":"10.2307\/2963594","volume":"22","author":"W Craig","year":"1957","unstructured":"Craig, W.: Three uses of the herbrand-gentzen theorem in relating model theory and proof theory. The Journal of Symbolic Logic 22(3), 269\u2013285 (1957)","journal-title":"The Journal of Symbolic Logic"},{"key":"13_CR7","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. 6012, pp. 185\u2013204. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-11957-6_11"},{"key":"13_CR8","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. 5944, pp. 129\u2013145. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-11319-2_12"},{"key":"13_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/11817963_11","volume-title":"Computer Aided Verification","author":"B Dutertre","year":"2006","unstructured":"Dutertre, B., de Moura, L.: A fast linear-arithmetic solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 81\u201394. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11817963_11"},{"key":"13_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"625","DOI":"10.1007\/978-3-662-49674-9_41","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Gao","year":"2016","unstructured":"Gao, S., Zufferey, D.: Interpolants in nonlinear theories over the reals. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 625\u2013641. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49674-9_41"},{"key":"13_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1007\/978-3-319-21690-4_20","volume-title":"Computer Aided Verification","author":"A Gurfinkel","year":"2015","unstructured":"Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The seahorn verification framework. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 343\u2013361. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_20"},{"key":"13_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/BFb0030832","volume-title":"Computing and Combinatorics","author":"G Huang","year":"1995","unstructured":"Huang, G.: Constructing craig interpolation formulas. In: Du, D.-Z., Li, M. (eds.) COCOON 1995. LNCS, vol. 959, pp. 181\u2013190. Springer, Heidelberg (1995). https:\/\/doi.org\/10.1007\/BFb0030832"},{"key":"13_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1007\/978-3-319-66263-3_22","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2017","author":"AEJ Hyv\u00e4rinen","year":"2017","unstructured":"Hyv\u00e4rinen, A.E.J., Asadi, S., Even-Mendoza, K., Fedyukovich, G., Chockler, H., Sharygina, N.: Theory refinement for program verification. In: Gaspers, S., Walsh, T. (eds.) SAT 2017. LNCS, vol. 10491, pp. 347\u2013363. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66263-3_22"},{"key":"13_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"547","DOI":"10.1007\/978-3-319-40970-2_35","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2016","author":"AEJ Hyv\u00e4rinen","year":"2016","unstructured":"Hyv\u00e4rinen, A.E.J., Marescotti, M., Alt, L., Sharygina, N.: OpenSMT2: an SMT solver for multi-core and cloud computing. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 547\u2013553. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-40970-2_35"},{"issue":"2","key":"13_CR15","doi-asserted-by":"crossref","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. Journal of Symbolic Logic 62(2), 457\u2013486 (1997)","journal-title":"Journal of Symbolic Logic"},{"key":"13_CR16","doi-asserted-by":"crossref","unstructured":"Kroening, D., Strichman, O.: Decision Procedures: An Algorithmic Point of View, 2nd edn. Texts in Theoretical Computer Science. An EATCS Series. Springer (2016)","DOI":"10.1007\/978-3-662-50497-0"},{"issue":"1","key":"13_CR17","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1016\/j.tcs.2005.07.003","volume":"345","author":"KL McMillan","year":"2005","unstructured":"McMillan, K.L.: An interpolating theorem prover. Theor. Comput. Sci. 345(1), 101\u2013121 (2005)","journal-title":"Theor. Comput. Sci."},{"key":"13_CR18","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":"KL McMillan","year":"2003","unstructured":"McMillan, K.L.: Interpolation and SAT-based model checking. In: Hunt, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 1\u201313. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45069-6_1"},{"issue":"3","key":"13_CR19","doi-asserted-by":"crossref","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. Journal of Symbolic Logic 62(3), 981\u2013998 (1997)","journal-title":"Journal of Symbolic Logic"},{"key":"13_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"683","DOI":"10.1007\/978-3-642-45221-5_45","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"SF Rollini","year":"2013","unstructured":"Rollini, S.F., Alt, L., Fedyukovich, G., Hyv\u00e4rinen, A.E.J., Sharygina, N.: PeRIPLO: a framework for producing effective interpolants in SAT-based software verification. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR 2013. LNCS, vol. 8312, pp. 683\u2013693. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-45221-5_45"},{"key":"13_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/978-3-642-31424-7_18","volume-title":"Computer Aided Verification","author":"SF Rollini","year":"2012","unstructured":"Rollini, S.F., Sery, O., Sharygina, N.: Leveraging interpolant strength in model checking. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 193\u2013209. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_18"},{"key":"13_CR22","doi-asserted-by":"crossref","unstructured":"R\u00fcmmer, P., Subotic, P.: Exploring interpolants. In: Proc. FMCAD 2013, pp. 69\u201376. IEEE (2013)","DOI":"10.1109\/FMCAD.2013.6679393"},{"key":"13_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1007\/978-3-540-69738-1_25","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A Rybalchenko","year":"2007","unstructured":"Rybalchenko, A., Sofronie-Stokkermans, V.: Constraint solving for interpolation. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 346\u2013362. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-69738-1_25"},{"issue":"1","key":"13_CR24","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/s10817-016-9364-6","volume":"57","author":"M Schlaipfer","year":"2016","unstructured":"Schlaipfer, M., Weissenbacher, G.: Labelled interpolation systems for hyper-resolution, clausal, and local proofs. Journal of Automated Reasoning 57(1), 3\u201336 (2016)","journal-title":"Journal of Automated Reasoning"},{"key":"13_CR25","doi-asserted-by":"crossref","unstructured":"Scholl, C., Pigorsch, F., Disch, S., Althaus, E.: Simple interpolants for linear arithmetic. In: Proc. DATE 2014, pp. 1\u20136. European Design and Automation Association (2014)","DOI":"10.7873\/DATE2014.128"}],"container-title":["Lecture Notes in Computer Science","Hardware and Software: Verification and Testing"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-70389-3_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,5]],"date-time":"2019-10-05T21:29:37Z","timestamp":1570310977000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-70389-3_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319703886","9783319703893"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-70389-3_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}