{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T13:34:10Z","timestamp":1760016850344,"version":"3.40.3"},"publisher-location":"Cham","reference-count":13,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319298160"},{"type":"electronic","value":"9783319298177"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[[2016]]},"DOI":"10.1007\/978-3-319-29817-7_2","type":"book-chapter","created":{"date-parts":[[2016,2,3]],"date-time":"2016-02-03T00:46:18Z","timestamp":1454460378000},"page":"11-22","source":"Crossref","is-referenced-by-count":1,"title":["Flexible Interpolation for Efficient Model Checking"],"prefix":"10.1007","author":[{"given":"Antti E. J.","family":"Hyv\u00e4rinen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Leonardo","family":"Alt","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Natasha","family":"Sharygina","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"2_CR1","doi-asserted-by":"crossref","unstructured":"Alt, L., Fedyukovich, G., Hyv\u00e4rinen, A.E.J., Sharygina, N.: A proof-sensitive approach for small propositional interpolants. In: Proceedings of VSTTE 2015 (2015, to appear)","DOI":"10.1007\/978-3-319-29613-5_1"},{"key":"2_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/978-3-642-01702-5_14","volume-title":"Hardware and Software: Verification and Testing","author":"O Bar-Ilan","year":"2009","unstructured":"Bar-Ilan, O., Fuhrmann, O., Hoory, S., Shacham, O., Strichman, O.: Linear-time reductions of resolution proofs. In: Chockler, H., Hu, A.J. (eds.) HVC 2008. LNCS, vol. 5394, pp. 114\u2013128. Springer, Heidelberg (2009)"},{"key":"2_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"A Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, p. 193. Springer, Heidelberg (1999)"},{"key":"2_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Logics of Programs","author":"E Clarke","year":"1982","unstructured":"Clarke, E., Emerson, E.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52\u201371. Springer, Heidelberg (1982)"},{"issue":"3","key":"2_CR5","doi-asserted-by":"publisher","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. J. Symbolic Logic 22(3), 269\u2013285 (1957)","journal-title":"J. Symbolic Logic"},{"issue":"3","key":"2_CR6","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M Davis","year":"1960","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM 7(3), 201\u2013215 (1960)","journal-title":"J. ACM"},{"issue":"3","key":"2_CR7","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1145\/1066100.1066102","volume":"52","author":"D Detlefs","year":"2005","unstructured":"Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. J. ACM 52(3), 365\u2013473 (2005)","journal-title":"J. ACM"},{"key":"2_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)"},{"key":"2_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"186","DOI":"10.1007\/978-3-662-46675-9_13","volume-title":"Fundamental Approaches to Software Engineering","author":"G Fedyukovich","year":"2015","unstructured":"Fedyukovich, G., D\u2019Iddio, A.C., Hyv\u00e4rinen, A.E.J., Sharygina, N.: Symbolic detection of assertion dependencies for bounded model checking. In: Egyed, A., Schaefer, I. (eds.) FASE 2015. LNCS, vol. 9033, pp. 186\u2013201. Springer, Heidelberg (2015)"},{"key":"2_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/978-3-642-22438-6_19","volume-title":"Automated Deduction \u2013 CADE-23","author":"P Fontaine","year":"2011","unstructured":"Fontaine, P., Merz, S., Woltzenlogel Paleo, B.: Compression of propositional resolution proofs via partial regularization. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol. 6803, pp. 237\u2013251. Springer, Heidelberg (2011)"},{"key":"2_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/978-3-540-24730-2_2","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"KL McMillan","year":"2004","unstructured":"McMillan, K.L.: An interpolating theorem prover. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 16\u201330. Springer, Heidelberg (2004)"},{"key":"2_CR12","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-19 2013. LNCS, vol. 8312, pp. 683\u2013693. Springer, Heidelberg (2013)"},{"issue":"1","key":"2_CR13","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10703-014-0208-x","volume":"45","author":"SF Rollini","year":"2014","unstructured":"Rollini, S.F., Bruttomesso, R., Sharygina, N., Tsitovich, A.: Resolution proof transformation for compression and interpolation. Formal Methods Syst. Des. 45(1), 1\u201341 (2014)","journal-title":"Formal Methods Syst. Des."}],"container-title":["Lecture Notes in Computer Science","Mathematical and Engineering Methods in Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-29817-7_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T08:37:46Z","timestamp":1559378266000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-29817-7_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319298160","9783319298177"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-29817-7_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}