{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T13:18:54Z","timestamp":1760015934874,"version":"3.40.3"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319296128"},{"type":"electronic","value":"9783319296135"}],"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-29613-5_1","type":"book-chapter","created":{"date-parts":[[2016,1,28]],"date-time":"2016-01-28T02:47:34Z","timestamp":1453949254000},"page":"1-18","source":"Crossref","is-referenced-by-count":11,"title":["A Proof-Sensitive Approach for Small Propositional Interpolants"],"prefix":"10.1007","author":[{"given":"Leonardo","family":"Alt","sequence":"first","affiliation":[]},{"given":"Grigory","family":"Fedyukovich","sequence":"additional","affiliation":[]},{"given":"Antti E. J.","family":"Hyv\u00e4rinen","sequence":"additional","affiliation":[]},{"given":"Natasha","family":"Sharygina","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"1_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)"},{"key":"1_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1007\/978-3-642-28717-6_7","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"F Alberti","year":"2012","unstructured":"Alberti, F., Bruttomesso, R., Ghilardi, S., Ranise, S., Sharygina, N.: Lazy abstraction with interpolants for arrays. In: Bj\u00f8rner, N., Voronkov, A. (eds.) LPAR-18 2012. LNCS, vol. 7180, pp. 46\u201361. Springer, Heidelberg (2012)"},{"key":"1_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"188","DOI":"10.1007\/978-3-319-13338-6_15","volume-title":"Hardware and Software: Verification and Testing","author":"R Bloem","year":"2014","unstructured":"Bloem, R., Malik, S., Schlaipfer, M., Weissenbacher, G.: Reduction of resolution refutations and interpolants via subsumption. In: Yahav, E. (ed.) HVC 2014. LNCS, vol. 8855, pp. 188\u2013203. Springer, Heidelberg (2014)"},{"key":"1_CR4","doi-asserted-by":"crossref","unstructured":"Cabodi, G., Lolacono, C., Vendraminetto, D.: Optimization techniques for Craig interpolant compaction in unbounded model checking. In: DATE, pp. 1417\u20131422 (2013)","DOI":"10.7873\/DATE.2013.289"},{"key":"1_CR5","doi-asserted-by":"crossref","unstructured":"Cabodi, G., Murciano, M., Nocco, S., Quer, S.: Stepping forward with interpolants in unbounded model checking. In: ICCAD, pp. 772\u2013778 (2006)","DOI":"10.1109\/ICCAD.2006.320119"},{"key":"1_CR6","doi-asserted-by":"crossref","unstructured":"Cabodi, G., Palena, M., Pasini, P.: Interpolation with guided refinement: revisiting incrementality in SAT-based unbounded model checking. In: FMCAD, pp. 43\u201350 (2014)","DOI":"10.1109\/FMCAD.2014.6987594"},{"key":"1_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/978-3-642-39611-3_12","volume-title":"Hardware and Software: Verification and Testing","author":"H Chockler","year":"2013","unstructured":"Chockler, H., Ivrii, A., Matsliah, A.: Computing interpolants without proofs. In: Biere, A., Nahir, A., Vos, T. (eds.) HVC. LNCS, vol. 7857, pp. 72\u201385. Springer, Heidelberg (2013)"},{"key":"1_CR8","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)"},{"key":"1_CR9","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":"1_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1007\/978-3-642-36742-7_21","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G Fedyukovich","year":"2013","unstructured":"Fedyukovich, G., Sery, O., Sharygina, N.: eVolCheck: incremental upgrade checker for C. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 292\u2013307. Springer, Heidelberg (2013)"},{"key":"1_CR11","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":"1_CR12","doi-asserted-by":"crossref","unstructured":"Janc\u00edk, P., Kofron, J., Rollini, S.F., Sharygina, N.: On interpolants and variable assignments. In: FMCAD, pp. 123\u2013130 (2014)","DOI":"10.1109\/FMCAD.2014.6987604"},{"key":"1_CR13","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. 2725, pp. 1\u201313. Springer, Heidelberg (2003)"},{"key":"1_CR14","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":"1_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"243","DOI":"10.1007\/978-3-319-08867-9_16","volume-title":"Computer Aided Verification","author":"KL McMillan","year":"2014","unstructured":"McMillan, K.L.: Lazy annotation revisited. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 243\u2013259. Springer, Heidelberg (2014)"},{"issue":"3","key":"1_CR16","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. Symbolic Logic 62(3), 981\u2013998 (1997)","journal-title":"J. Symbolic Logic"},{"key":"1_CR17","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)"},{"key":"1_CR18","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)"},{"key":"1_CR19","doi-asserted-by":"crossref","unstructured":"R\u00fcmmer, P., Subotic, P.: Exploring interpolants. In: FMCAD, pp. 69\u201376 (2013)","DOI":"10.1109\/FMCAD.2013.6679393"},{"key":"1_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/978-3-642-33386-6_17","volume-title":"Automated Technology for Verification and Analysis","author":"O Sery","year":"2012","unstructured":"Sery, O., Fedyukovich, G., Sharygina, N.: FunFrog: bounded model checking with interpolation-based function summarization. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, vol. 7561, pp. 203\u2013207. Springer, Heidelberg (2012)"},{"key":"1_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"330","DOI":"10.1007\/978-3-642-39799-8_23","volume-title":"Computer Aided Verification","author":"Y Vizel","year":"2013","unstructured":"Vizel, Y., Ryvchin, V., Nadel, A.: Efficient generation of small interpolants in CNF. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 330\u2013346. Springer, Heidelberg (2013)"}],"container-title":["Lecture Notes in Computer Science","Verified Software: Theories, Tools, and Experiments"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-29613-5_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T07:51:59Z","timestamp":1559375519000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-29613-5_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319296128","9783319296135"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-29613-5_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}