{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,11]],"date-time":"2026-03-11T00:34:46Z","timestamp":1773189286209,"version":"3.50.1"},"reference-count":53,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017,10]]},"DOI":"10.1109\/ase.2017.8115690","type":"proceedings-article","created":{"date-parts":[[2017,11,23]],"date-time":"2017-11-23T22:03:57Z","timestamp":1511474637000},"page":"793-803","source":"Crossref","is-referenced-by-count":14,"title":["FiB: Squeezing loop invariants by interpolation between forward\/backward predicate transformers"],"prefix":"10.1109","author":[{"given":"Shang-Wei","family":"Lin","sequence":"first","affiliation":[]},{"given":"Jun","family":"Sun","sequence":"additional","affiliation":[]},{"given":"Hao","family":"Xiao","sequence":"additional","affiliation":[]},{"given":"Yang","family":"Liu","sequence":"additional","affiliation":[]},{"given":"David","family":"Sanan","sequence":"additional","affiliation":[]},{"given":"Henri","family":"Hansen","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-8(3:25)2012"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-93900-9_20"},{"key":"ref33","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1007\/3-540-44829-2_17","article-title":"Software verification with BLAST","volume":"5403","author":"henzinger","year":"2003","journal-title":"International Conference on Model Checking Software (SPIN)"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964021"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_48"},{"key":"ref30","first-page":"120","article-title":"Constraint-based invariant inference over predicate abstraction","author":"gulwani","year":"2009","journal-title":"Verification Model Checking and Abstract Interpretation volume 5403 of LNCS"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1007\/BF00268497"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1007\/11691372_33"},{"key":"ref35","author":"jeannet","year":"0","journal-title":"Interproc Analyzer for Recursive Programs with Numerical Variables"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328468"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1007\/11691372_34"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375616"},{"key":"ref2","year":"0"},{"key":"ref1","year":"0"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509511"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45251-6_29"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.01.015"},{"key":"ref24","first-page":"69","article-title":"Ice: A robust framework for learning invariants","author":"garg","year":"2014","journal-title":"CAV"},{"key":"ref23","first-page":"19","article-title":"Assigning meanings to programs","volume":"xix","author":"floyd","year":"1967","journal-title":"Applied Math"},{"key":"ref26","first-page":"377","article-title":"Abductive analysis of modular logic programs","author":"giacobazzi","year":"1994","journal-title":"International Symposium on Logic Programming"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837664"},{"key":"ref50","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_31"},{"key":"ref51","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38856-9_21"},{"key":"ref53","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/3054.001.0001","author":"winskel","year":"1993","journal-title":"The Formal Semantics of Programming Languages An Introduction"},{"key":"ref52","first-page":"308","article-title":"Intertwined forward-backward reachability analysis using interpolants","author":"vizel","year":"2013","journal-title":"TACAS"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31612-8_1"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1145\/1594834.1480917"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2015.33"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10672-9_19"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1145\/876638.876643"},{"key":"ref14","author":"clarke","year":"1999","journal-title":"Model checking"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45069-6_39"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1145\/567752.567778"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1145\/512760.512770"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.2307\/2963594"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-3228-5"},{"key":"ref4","year":"0"},{"key":"ref3","year":"0"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_22"},{"key":"ref5","year":"0"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250769"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44585-4_25"},{"key":"ref49","first-page":"88","article-title":"From invariant checking to invariant inference using randomized search","volume":"8559","author":"sharma","year":"2014","journal-title":"CAV"},{"key":"ref9","first-page":"184","article-title":"CPAchecker: A tool for configurable software verification","author":"beyer","year":"2011","journal-title":"CAV"},{"key":"ref46","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-015-0333-3"},{"key":"ref45","author":"peirce","year":"1932","journal-title":"Collected Papers of Charles Sanders Peirce"},{"key":"ref48","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964028"},{"key":"ref47","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2006.03.003"},{"key":"ref42","first-page":"123","article-title":"Lazy abstraction with interpolants","volume":"4144","author":"mcmillan","year":"2006","journal-title":"CAV"},{"key":"ref41","first-page":"1","article-title":"Interpolation and SAT-based model checking","volume":"2725","author":"mcmillan","year":"2003","journal-title":"CAV"},{"key":"ref44","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-006-8609-1"},{"key":"ref43","first-page":"104","article-title":"Lazy annotation for program testing and verification","volume":"6174","author":"mcmillan","year":"2010","journal-title":"CAV"}],"event":{"name":"2017 32nd IEEE\/ACM International Conference on Automated Software Engineering (ASE)","location":"Urbana, IL","start":{"date-parts":[[2017,10,30]]},"end":{"date-parts":[[2017,11,3]]}},"container-title":["2017 32nd IEEE\/ACM International Conference on Automated Software Engineering (ASE)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/8106906\/8115603\/08115690.pdf?arnumber=8115690","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,8]],"date-time":"2022-08-08T05:53:05Z","timestamp":1659937985000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/8115690\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,10]]},"references-count":53,"URL":"https:\/\/doi.org\/10.1109\/ase.2017.8115690","relation":{},"subject":[],"published":{"date-parts":[[2017,10]]}}}