{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T12:59:13Z","timestamp":1770296353553,"version":"3.49.0"},"reference-count":21,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013,11]]},"DOI":"10.1109\/ase.2013.6693074","type":"proceedings-article","created":{"date-parts":[[2014,1,6]],"date-time":"2014-01-06T17:07:25Z","timestamp":1389028045000},"page":"136-146","source":"Crossref","is-referenced-by-count":28,"title":["BLITZ: Compositional bounded model checking for real-world programs"],"prefix":"10.1109","author":[{"given":"Chia Yuan","family":"Cho","sequence":"first","affiliation":[]},{"given":"Vijay","family":"D'Silva","sequence":"additional","affiliation":[]},{"given":"Dawn","family":"Song","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"19","doi-asserted-by":"publisher","DOI":"10.1109\/ISSRE.2010.27"},{"key":"17","doi-asserted-by":"crossref","first-page":"104","DOI":"10.1007\/978-3-642-14295-6_10","article-title":"Lazy annotation for program testing and verification","author":"mcmillan","year":"2010","journal-title":"Computer Aided Verification"},{"key":"18","doi-asserted-by":"crossref","first-page":"138","DOI":"10.1007\/978-3-642-24690-6_11","article-title":"A dataflow analysis to improve sat-based bounded program verification","author":"parrino","year":"2011","journal-title":"Proceedings of the 9th International Conference on Software Engineering and Formal Methods SEFM'11"},{"key":"15","first-page":"1","article-title":"Interpolation and SAT-based model checking","author":"mcmillan","year":"2003","journal-title":"Conference on Computer Aided Verification"},{"key":"16","first-page":"123","article-title":"Lazy abstraction with interpolants","volume":"4144","author":"mcmillan","year":"2006","journal-title":"Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)"},{"key":"13","article-title":"On computing minimum unsatisfiable cores","author":"lynce","year":"2004","journal-title":"Conference on Theory and Applications of Satisfiability Testing Online Proceedings"},{"key":"14","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328440"},{"key":"11","doi-asserted-by":"crossref","first-page":"427","DOI":"10.1007\/978-3-642-31424-7_32","article-title":"A solver for reachability modulo theories","author":"lal","year":"2012","journal-title":"Proceedings of the 24th International Conference on Computer Aided Verification"},{"key":"12","article-title":"Bugbench: Benchmarks for evaluating bug detection tools","author":"lu","year":"2005","journal-title":"Workshop on the Evaluation of Software Defect Detection Tools"},{"key":"21","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_42"},{"key":"3","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378846"},{"key":"20","first-page":"757","article-title":"An incremental approach to scope-bounded checking using a lightweight formal method","author":"shao","year":"2009","journal-title":"Proceedings of the 2nd World Congress on Formal Methods FM '09"},{"key":"2","doi-asserted-by":"publisher","DOI":"10.1145\/1368088.1368118"},{"key":"1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_28"},{"key":"10","doi-asserted-by":"crossref","first-page":"573","DOI":"10.1007\/978-3-642-22110-1_45","article-title":"Interpolation-based software verification with wolverine","author":"kroening","year":"2011","journal-title":"Proceedings of the 23rd International Conference on Computer Aided Verification CAV'11"},{"key":"7","first-page":"502","article-title":"An extensible SAT-solver","author":"ee?n","year":"2003","journal-title":"Enrico Giunchiglia and Armando Tacchella"},{"key":"6","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","article-title":"Z3: An efficient SMT solver","author":"de moura","year":"2008","journal-title":"TACAS'08 Proc of the 14th Int Conf on Tools and Algorithms for the Construction and Analysis of Systems"},{"key":"5","doi-asserted-by":"publisher","DOI":"10.1145\/775832.775928"},{"key":"4","doi-asserted-by":"crossref","first-page":"70","DOI":"10.1007\/978-3-642-18275-4_7","article-title":"SAT-based model checking without unrolling","author":"bradley","year":"2011","journal-title":"Proceedings of the 12th International Conference on Verification Model Checking and Abstract Interpretation VMCAI'11"},{"key":"9","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"8","doi-asserted-by":"publisher","DOI":"10.1145\/1707801.1706307"}],"event":{"name":"2013 IEEE\/ACM 28th International Conference on Automated Software Engineering (ASE)","location":"Silicon Valley, CA, USA","start":{"date-parts":[[2013,11,11]]},"end":{"date-parts":[[2013,11,15]]}},"container-title":["2013 28th IEEE\/ACM International Conference on Automated Software Engineering (ASE)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/6684409\/6693054\/06693074.pdf?arnumber=6693074","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T11:20:03Z","timestamp":1746098403000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/6693074\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,11]]},"references-count":21,"URL":"https:\/\/doi.org\/10.1109\/ase.2013.6693074","relation":{},"subject":[],"published":{"date-parts":[[2013,11]]}}}