{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:26:06Z","timestamp":1740122766602,"version":"3.37.3"},"reference-count":32,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2019,11,7]],"date-time":"2019-11-07T00:00:00Z","timestamp":1573084800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2019,11,7]],"date-time":"2019-11-07T00:00:00Z","timestamp":1573084800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100001824","name":"Grantov\u00e1 Agentura Cesk\u00e9 Republiky","doi-asserted-by":"publisher","award":["18-17403S"],"award-info":[{"award-number":["18-17403S"]}],"id":[{"id":"10.13039\/501100001824","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2019,12]]},"DOI":"10.1007\/s10703-019-00342-z","type":"journal-article","created":{"date-parts":[[2019,11,7]],"date-time":"2019-11-07T19:03:05Z","timestamp":1573153385000},"page":"33-71","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Exploiting partial variable assignment in interpolation-based model checking"],"prefix":"10.1007","volume":"55","author":[{"given":"Pavel","family":"Jan\u010d\u00edk","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0391-4812","authenticated-orcid":false,"given":"Jan","family":"Kofro\u0148","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Leonardo","family":"Alt","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Grigory","family":"Fedyukovich","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Antti E. J.","family":"Hyv\u00e4rinen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Natasha","family":"Sharygina","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,11,7]]},"reference":[{"key":"342_CR1","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/978-3-642-28756-5_12","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Aws Albarghouthi","year":"2012","unstructured":"Albarghouthi A, Gurfinkel A, Chechik M (2012) From under-approximations to over-approximations and back. In: Flanagan C, K\u00f6nig B (eds) Tools and algorithms for the construction and analysis of systems\u201418th international conference, TACAS 2012, held as part of the European joint conferences on theory and practice of software, ETAPS 2012, Tallinn, Estonia, Mar 24\u2013Apr 1, 2012. Proceedings, volume 7214 of Lecture notes in computer science. Springer, pp 157\u2013172"},{"key":"342_CR2","doi-asserted-by":"crossref","unstructured":"Albarghouthi A, Gurfinkel A, Chechik M (2012) Whale: an interpolation-based algorithm for inter-procedural verification. In: Kuncak V, Rybalchenko A (eds) Verification, model checking, and abstract interpretation\u201413th international conference, VMCAI 2012, Philadelphia, PA, USA, 22\u201324 Jan 2012. Proceedings, volume 7148 of Lecture notes in computer science. Springer, pp 39\u201355","DOI":"10.1007\/978-3-642-27940-9_4"},{"key":"342_CR3","doi-asserted-by":"crossref","unstructured":"Albarghouthi A, Li Y, Gurfinkel A, Chechik M (2012) UFO: a framework for abstraction- and interpolation-based software verification. In: Madhusudan P and Seshia SA (Eds) Computer aided verification\u201424th international conference, CAV 2012, Berkeley, CA, USA, 7\u201313 July 2012, proceedings, volume 7358 of Lecture notes in computer science. Springer, pp 672\u2013678","DOI":"10.1007\/978-3-642-31424-7_48"},{"key":"342_CR4","unstructured":"Barrett C, Stump A, Tinelli C (2010) The SMT-LIB standard: version 2.0. Technical report, Department of Computer Science, The University of Iowa. \nhttp:\/\/www.SMT-LIB.org"},{"key":"#cr-split#-342_CR5.1","doi-asserted-by":"crossref","unstructured":"Cabodi G, Loiacono C, Vendraminetto D (2013) Optimization techniques for Craig interpolant compaction in unbounded model checking. In: Enrico M","DOI":"10.7873\/DATE.2013.289"},{"key":"#cr-split#-342_CR5.2","unstructured":"(ed) Design. Automation and test in Europe, DATE 13, Grenoble, France, 18-22 Mar 2013. EDA Consortium San Jose, CA, USA\/ACM DL, pp 1417-1422"},{"issue":"3","key":"342_CR6","doi-asserted-by":"publisher","first-page":"269","DOI":"10.2307\/2963594","volume":"22","author":"W Craig","year":"1957","unstructured":"Craig W (1957) Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory. J Symb Log 22(3):269\u2013285","journal-title":"J Symb Log"},{"key":"342_CR7","doi-asserted-by":"crossref","unstructured":"D\u2019Silva V, Kroening D, Purandare M, Weissenbacher G (2010) Interpolant strength. In: Barthe G, Hermenegildo MV (eds) Verification, model checking, and abstract interpretation, 11th international conference, VMCAI 2010, Madrid, Spain, 17\u201319 Jan 2010. Proceedings, volume 5944 of Lecture notes in computer science. Springer, pp 129\u2013145","DOI":"10.1007\/978-3-642-11319-2_12"},{"key":"342_CR8","doi-asserted-by":"crossref","unstructured":"E\u00e9n N, Biere A (2005) Effective preprocessing in SAT through variable and clause elimination. In: Bacchus F, Walsh T (eds) Theory and applications of satisfiability testing, 8th international conference, SAT 2005, St. Andrews, UK, 19\u201323 June 2005. Proceedings, volume 3569 of Lecture notes in computer science. Springer, pp 61\u201375","DOI":"10.1007\/11499107_5"},{"key":"342_CR9","doi-asserted-by":"crossref","unstructured":"Fedyukovich G, Sery O, Sharygina N (2013) eVolCheck: incremental upgrade checker for C. In: Piterman N, Smolka SA (eds) Tools and algorithms for the construction and analysis of systems\u201419th international conference, TACAS 2013, held as part of the European joint conferences on theory and practice of software, ETAPS 2013, Rome, Italy, 16\u201324 Mar 2013. Proceedings, volume 7795 of Lecture notes in computer science. Springer, pp 292\u2013307","DOI":"10.1007\/978-3-642-36742-7_21"},{"key":"342_CR10","doi-asserted-by":"crossref","unstructured":"Gurfinkel A, Rollini SF, Sharygina N (2013) Interpolation properties and SAT-based model checking. In: Van Hung D, Ogawa M (eds) Automated technology for verification and analysis\u201411th international symposium, ATVA 2013, Hanoi, Vietnam, 15\u201318 Oct 2013. Proceedings, volume 8172 of Lecture notes in computer science. Springer, pp 255\u2013271","DOI":"10.1007\/978-3-319-02444-8_19"},{"key":"342_CR11","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":"Antti E. J. Hyv\u00e4rinen","year":"2016","unstructured":"Hyv\u00e4rinen AEJ, Marescotti M, Alt L, Sharygina N (2016) OpenSMT2: an SMT solver for multi-core and cloud computing. In: Creignou N, Le\u00a0Berre D (eds) Theory and applications of satisfiability testing\u2014SAT 2016: 19th international conference, Bordeaux, France, 5\u20138 July 2016, Proceedings. Springer, Cham, pp 547\u2013553"},{"key":"342_CR12","doi-asserted-by":"publisher","first-page":"419","DOI":"10.1007\/978-3-662-49665-7_25","volume-title":"Fundamental Approaches to Software Engineering","author":"Pavel Jan\u010d\u00edk","year":"2016","unstructured":"Jan\u010d\u00edk P, Alt L, Fedyukovich G, Hyv\u00e4rinen AEJ, Kofro\u0148 J, Sharygina N (2016) PVAIR: Partial Variable Assignment InterpolatoR. In: Fundamental approaches to software engineering (FASE) 2016, LNCS 9633. Springer, Berlin, Heidelberg, pp 419\u2013434"},{"key":"342_CR13","unstructured":"Jan\u010d\u00edk P, Kofro\u0148 J, Rollini SF, Sharygina N (2014) On interpolants and variable assignments. In: Formal methods in computer-aided design, FMCAD 2014, Lausanne, Switzerland, 21\u201324 Oct 2014. IEEE, pp 123\u2013130"},{"key":"342_CR14","doi-asserted-by":"crossref","unstructured":"Madhusudan P, Seshia SA (eds) (2012) Computer aided verification\u201424th international conference, CAV 2012, Berkeley, CA, USA, 7\u201313 July 2012. Proceedings, volume 7358 of Lecture notes in computer science. Springer","DOI":"10.1007\/978-3-642-31424-7"},{"key":"342_CR15","doi-asserted-by":"crossref","unstructured":"McMillan KL (2003) Interpolation and SAT-based model checking. In: Hunt WA Jr, Somenzi F (eds) Computer aided verification, 15th international conference, CAV 2003, Boulder, CO, USA, 8\u201312 July 2003, proceedings, volume 2725 of Lecture notes in computer science. Springer, pp 1\u201313","DOI":"10.1007\/978-3-540-45069-6_1"},{"key":"342_CR16","doi-asserted-by":"crossref","unstructured":"McMillan KL (2006) Lazy abstraction with interpolants. In: Ball T, Jones RB (eds) Computer aided verification, 18th international conference, CAV 2006, Seattle, WA, USA, 17\u201320 Aug 2006, proceedings, volume 4144 of Lecture notes in computer science. Springer, pp 123\u2013136","DOI":"10.1007\/11817963_14"},{"issue":"3","key":"342_CR17","doi-asserted-by":"publisher","first-page":"981","DOI":"10.2307\/2275583","volume":"62","author":"P Pavel","year":"1997","unstructured":"Pavel P (1997) Lower bounds for resolution and cutting plane proofs and monotone computations. J Symb Log 62(3):981\u2013998","journal-title":"J Symb Log"},{"key":"342_CR18","unstructured":"Rollini S, Bruttomesso R, Sharygina N (2010) An efficient and flexible approach to resolution proof reduction. In: Barner S, Harris IG, Kroening D, Raz O (eds) Hardware and software: verification and testing\u20146th international Haifa verification conference, HVC 2010, Haifa, Israel, 4\u20137 Oct 2010. Revised selected papers, volume 6504 of Lecture notes in computer science. Springer, pp 182\u2013196"},{"key":"342_CR19","doi-asserted-by":"crossref","unstructured":"Rollini SF, Alt L, Fedyukovich G, Hyv\u00e4rinen AEJ, Sharygina N (2013) PeRIPLO: a framework for producing effective interpolants in SAT-based software verification. In: McMillan KL, Middeldorp A, Voronkov A (eds) Logic for programming, artificial intelligence, and reasoning\u201419th international conference, LPAR-19, Stellenbosch, South Africa, 14\u201319 Dec 2013. Proceedings, volume 8312 of Lecture notes in computer science. Springer, pp 683\u2013693","DOI":"10.1007\/978-3-642-45221-5_45"},{"issue":"1","key":"342_CR20","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10703-014-0208-x","volume":"45","author":"SF Rollini","year":"2014","unstructured":"Rollini SF, Bruttomesso R, Sharygina N, Tsitovich A (2014) resolution proof transformation for compression and interpolation. Form Methods Syst Des 45(1):1\u201341","journal-title":"Form Methods Syst Des"},{"key":"342_CR21","doi-asserted-by":"crossref","unstructured":"Rollini SF, Sery O, Sharygina N (2012) Leveraging interpolant strength in model checking. In: Madhusudan P, Seshia SA (eds) Computer aided verification\u201424th international conference, CAV 2012, Berkeley, CA, USA, 7\u201313 July 2012, proceedings, volume 7358 of Lecture notes in computer science. Springer, pp 193\u2013209","DOI":"10.1007\/978-3-642-31424-7_18"},{"key":"342_CR22","doi-asserted-by":"crossref","unstructured":"R\u00fcmmer P, Hojjat H, Kuncak V (2014) Classifying and solving horn clauses for verification. In: Cohen E, Rybalchenko A (eds) Verified software: theories, tools, experiments: 5th international conference, VSTTE 2013, Menlo Park, CA, USA, 17\u201319 May 2013, revised selected papers. Springer, Berlin, pp 1\u201321","DOI":"10.1007\/978-3-642-54108-7_1"},{"key":"342_CR23","unstructured":"SAT competition. \nhttp:\/\/www.satcompetition.org\/"},{"key":"342_CR24","unstructured":"Sery O, Fedyukovich G, Sharygina N (2012) Incremental upgrade checking by means of interpolation-based function summaries. In: 2012 formal methods in computer-aided design (FMCAD), pp 114\u2013121"},{"key":"342_CR25","doi-asserted-by":"crossref","unstructured":"Sery O, Fedyukovich G, Sharygina N (2012) FunFrog: bounded model checking with interpolation-based function summarization. In: Chakraborty S, Mukund M (eds) Automated technology for verification and analysis\u201410th international symposium, ATVA 2012, Thiruvananthapuram, India, 3\u20136 Oct 2012. Proceedings, volume 7561 of Lecture notes in computer science. Springer, pp 203\u2013207","DOI":"10.1007\/978-3-642-33386-6_17"},{"key":"342_CR26","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/978-3-642-34188-5_15","volume-title":"Hardware and Software: Verification and Testing","author":"Ondrej Sery","year":"2012","unstructured":"Sery O, Fedyukovich G, Sharygina N (2012) Interpolation-based function summaries in bounded model checking. In: Eder K, Louren\u00e7o J, Shehory O (eds) Hardware and software: verification and testing: 7th international Haifa verification conference, HVC 2011, Haifa, Israel, 6\u20138 Dec 2011, revised selected papers. Springer Berlin, pp 160\u2013175"},{"issue":"1","key":"342_CR27","first-page":"42","volume":"36","author":"O Tange","year":"2011","unstructured":"Tange O (2011) GNU parallel\u2014the command-line power tool. USENIX Mag 36(1):42\u201347","journal-title":"USENIX Mag"},{"key":"342_CR28","first-page":"89","volume-title":"Abstract model checking without computing the abstraction","author":"S Tonetta","year":"2009","unstructured":"Tonetta S (2009) Abstract model checking without computing the abstraction. Springer, Berlin, pp 89\u2013105"},{"key":"342_CR29","doi-asserted-by":"crossref","unstructured":"Tseitin GS (1969) On the complexity of derivation in propositional calculus. In: Studies in constructive mathematics and mathematical logic, part II, volume 8 of seminars in mathematics, V. A. Steklov Mathematical Institute, Leningrad. Consultants Bureau","DOI":"10.1007\/978-1-4899-5327-8_25"},{"key":"342_CR30","doi-asserted-by":"crossref","unstructured":"Vizel Y, Grumberg O (2009) Interpolation-sequence based model checking. In: Proceedings of 9th international conference on formal methods in computer-aided design, FMCAD 2009, 15\u201318 Nov 2009, Austin, Texas, USA. IEEE, pp 1\u20138","DOI":"10.1109\/FMCAD.2009.5351148"},{"key":"342_CR31","doi-asserted-by":"publisher","first-page":"641","DOI":"10.1007\/978-3-319-21690-4_43","volume-title":"Computer Aided Verification","author":"Yakir Vizel","year":"2015","unstructured":"Vizel Y, Gurfinkel A, Malik S (2015) Fast interpolating BMC. In: Kroening D, P\u0103s\u0103reanu CS (eds) Computer aided verification, number 9206 in Lecture notes in computer science. Springer, pp 641\u2013657. \nhttps:\/\/doi.org\/10.1007\/978-3-319-21690-4_43"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-019-00342-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-019-00342-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-019-00342-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,6]],"date-time":"2020-11-06T00:12:31Z","timestamp":1604621551000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-019-00342-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,11,7]]},"references-count":32,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2019,12]]}},"alternative-id":["342"],"URL":"https:\/\/doi.org\/10.1007\/s10703-019-00342-z","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2019,11,7]]},"assertion":[{"value":"7 November 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}