{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,8]],"date-time":"2026-07-08T22:32:14Z","timestamp":1783549934071,"version":"3.55.0"},"reference-count":24,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010,11]]},"DOI":"10.1109\/iccad.2010.5654297","type":"proceedings-article","created":{"date-parts":[[2010,12,10]],"date-time":"2010-12-10T22:29:13Z","timestamp":1292020153000},"page":"770-777","source":"Crossref","is-referenced-by-count":10,"title":["Flexible interpolation with local proof transformations"],"prefix":"10.1109","author":[{"given":"Roberto","family":"Bruttomesso","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Simone","family":"Rollini","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Natasha","family":"Sharygina","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Aliaksei","family":"Tsitovich","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"263","reference":[{"key":"19","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24730-2_2"},{"key":"22","doi-asserted-by":"publisher","DOI":"10.1145\/357073.357079"},{"key":"17","first-page":"39","article-title":"Interpolant-based transition relation approximation","author":"jhala","year":"2005","journal-title":"CAV"},{"key":"23","doi-asserted-by":"publisher","DOI":"10.2307\/2275583"},{"key":"18","first-page":"1","article-title":"Interpolation and SAT-based model checking","author":"mcmillan","year":"2003","journal-title":"CAV"},{"key":"24","doi-asserted-by":"publisher","DOI":"10.1007\/11532231_26"},{"key":"15","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02959-2_16"},{"key":"16","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964021"},{"key":"13","first-page":"129","article-title":"Interpolant strength","author":"d'silva","year":"2010","journal-title":"VMCAI"},{"key":"14","doi-asserted-by":"publisher","DOI":"10.1145\/1512464.1512468"},{"key":"11","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2009.5351142"},{"key":"12","article-title":"Restructuring resolution refutations for interpolation","author":"d'silva","year":"2008","journal-title":"Technical Report"},{"key":"21","article-title":"Lemmas on demand for satisfiability solvers","author":"de moura","year":"2002","journal-title":"SAT"},{"key":"3","doi-asserted-by":"publisher","DOI":"10.1007\/11916277_35"},{"key":"20","first-page":"22","article-title":"Applications of craig interpolation to model checking","author":"mcmillan","year":"2004","journal-title":"CSL"},{"key":"2","first-page":"114","article-title":"Linear-time reductions of resolution proofs","author":"bar-ilan","year":"2008","journal-title":"HVC"},{"key":"1","article-title":"Solvable cases of the decision problem","author":"ackermann","year":"1954","journal-title":"Studies in Logic and the Foundations of Mathematics"},{"key":"10","doi-asserted-by":"publisher","DOI":"10.2307\/2963594"},{"key":"7","doi-asserted-by":"publisher","DOI":"10.1145\/1512464.1512467"},{"key":"6","first-page":"335","article-title":"Efficient satisfiability modulo theories via delayed theory combination","author":"bozzano","year":"2005","journal-title":"CAV'05"},{"key":"5","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2008.ECP.18"},{"key":"4","volume":"185","author":"barrett","year":"2009","journal-title":"Handbook on Satisfiability"},{"key":"9","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_30"},{"key":"8","article-title":"The OpenSMT solver","author":"bruttomesso","year":"2010","journal-title":"TACAS"}],"event":{"name":"2010 IEEE\/ACM International Conference on Computer-Aided Design (ICCAD)","location":"San Jose, CA, USA","start":{"date-parts":[[2010,11,7]]},"end":{"date-parts":[[2010,11,11]]}},"container-title":["2010 IEEE\/ACM International Conference on Computer-Aided Design (ICCAD)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/5638200\/5648785\/05654297.pdf?arnumber=5654297","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,3,21]],"date-time":"2017-03-21T06:34:19Z","timestamp":1490078059000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/5654297\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,11]]},"references-count":24,"URL":"https:\/\/doi.org\/10.1109\/iccad.2010.5654297","relation":{},"subject":[],"published":{"date-parts":[[2010,11]]}}}