{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,3]],"date-time":"2025-05-03T16:28:49Z","timestamp":1746289729737,"version":"3.28.0"},"reference-count":39,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017,10]]},"DOI":"10.1109\/ase.2017.8115631","type":"proceedings-article","created":{"date-parts":[[2017,11,23]],"date-time":"2017-11-23T22:03:57Z","timestamp":1511474637000},"page":"183-193","source":"Crossref","is-referenced-by-count":7,"title":["More effective interpolations in software model checking"],"prefix":"10.1109","author":[{"given":"Cong","family":"Tian","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhao","family":"Duan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhenhua","family":"Duan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"C.-H. Luke","family":"Ong","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28756-5_41"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-23404-5_3"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32759-9_17"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28756-5_38"},{"key":"ref31","first-page":"218","article-title":"Applicability of the blast model checker: An industrial case study","author":"kolb","year":"2009","journal-title":"International Andrei Ershov Memorial Conference on Perspectives of System Informatics"},{"journal-title":"Bugs found in linux kernel with CPAChekcer","year":"0","key":"ref30"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28756-5_47"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_42"},{"journal-title":"The Science of Programming","year":"2012","author":"gries","key":"ref35"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_22"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.2307\/2963593"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_14"},{"key":"ref12","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1109\/FMCAD.2009.5351147","article-title":"Software model checking via large-block encoding","author":"beyer","year":"2009","journal-title":"Formal Methods in Computer-Aided Design 2009 FMCAD 2009"},{"key":"ref13","first-page":"189","article-title":"Predicate abstraction with adjustable-block encoding","author":"beyer","year":"2010","journal-title":"Proceedings of the 2010 Conference on Formal Methods in Computer-Aided Design"},{"key":"ref14","first-page":"1","article-title":"Interpolation and SAT-based model checking","author":"mcmillan","year":"2003","journal-title":"International Conference on Computer Aided Verification"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2009.5351148"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37057-1_11"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_11"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-015-0229-0"},{"key":"ref19","first-page":"31","article-title":"Program verification via Craig interpolation for Presburger arithmetic with arrays","author":"brillout","year":"2010","journal-title":"VERIFY IJCAR"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503279"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1145\/876638.876643"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49674-9_55"},{"key":"ref3","first-page":"1","article-title":"Model checking and the state explosion problem","author":"edmund","year":"2011","journal-title":"Software Engineering Proceedings of the LASER Summer School"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503274"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_21"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44829-2_17"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2013.6606566"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2014.2357442"},{"key":"ref2","doi-asserted-by":"crossref","first-page":"1512","DOI":"10.1145\/186025.186051","article-title":"Model checking and abstraction","volume":"16","author":"edmund","year":"1994","journal-title":"ACM Transactions on Programming Languages and Systems (TOPLAS)"},{"key":"ref9","first-page":"106","article-title":"Algorithms for software model checking: Predicate abstraction vs. Impact","author":"beyer","year":"2012","journal-title":"2012 Formal Methods in Computer-Aided Design (FMCAD) FMCAD"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1145\/1592434.1592438"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27940-9_4"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_10"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1145\/2491411.2491425"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2013.6679412"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-13338-6_14"},{"key":"ref26","first-page":"401","article-title":"Software verification and verifiable witnesses (Report on SV-COMP 2015)","author":"beyer","year":"2015","journal-title":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964021"}],"event":{"name":"2017 32nd IEEE\/ACM International Conference on Automated Software Engineering (ASE)","start":{"date-parts":[[2017,10,30]]},"location":"Urbana, IL","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\/08115631.pdf?arnumber=8115631","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,6]],"date-time":"2019-10-06T18:31:31Z","timestamp":1570386691000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/8115631\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,10]]},"references-count":39,"URL":"https:\/\/doi.org\/10.1109\/ase.2017.8115631","relation":{},"subject":[],"published":{"date-parts":[[2017,10]]}}}