{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,1]],"date-time":"2026-04-01T14:23:26Z","timestamp":1775053406446,"version":"3.50.1"},"reference-count":28,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011,11]]},"DOI":"10.1109\/ase.2011.6100046","type":"proceedings-article","created":{"date-parts":[[2011,12,16]],"date-time":"2011-12-16T18:30:08Z","timestamp":1324060208000},"page":"133-142","source":"Crossref","is-referenced-by-count":15,"title":["DC2: A framework for scalable, scope-bounded software verification"],"prefix":"10.1109","author":[{"given":"Franjo","family":"Ivancic","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gogul","family":"Balakrishnan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Aarti","family":"Gupta","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sriram","family":"Sankaranarayanan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Naoto","family":"Maeda","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hiroki","family":"Tokuoka","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Takashi","family":"Imoto","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yoshiaki","family":"Miyazaki","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"19","doi-asserted-by":"publisher","DOI":"10.1145\/1592434.1592438"},{"key":"17","doi-asserted-by":"publisher","DOI":"10.1145\/1134285.1134319"},{"key":"18","article-title":"Model checking C programs using F-Soft","author":"ivanc?ic?","year":"2005","journal-title":"ICCD"},{"key":"15","doi-asserted-by":"publisher","DOI":"10.1145\/781131.781149"},{"key":"16","doi-asserted-by":"publisher","DOI":"10.1145\/512557.512558"},{"key":"13","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"14","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-18275-4_12"},{"key":"11","article-title":"A tool for checking ANSI-C programs","author":"clarke","year":"2004","journal-title":"TACAS"},{"key":"12","article-title":"VCC: A practical system for verifying concurrent C","author":"cohen","year":"2009","journal-title":"TPHOLS"},{"key":"21","doi-asserted-by":"publisher","DOI":"10.1145\/1390630.1390657"},{"key":"20","author":"kurshan","year":"1994","journal-title":"Computer-Aided Verification of Coordinating Processes The Automata-Theoretic Approach"},{"key":"22","doi-asserted-by":"publisher","DOI":"10.1109\/WCRE.2001.957836"},{"key":"23","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2010.06.004"},{"key":"24","article-title":"An incremental approach to scope-bounded checking using a lightweight formal method","author":"shao","year":"2009","journal-title":"FM"},{"key":"25","doi-asserted-by":"publisher","DOI":"10.1007\/s10515-006-0005-x"},{"key":"26","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2003.1240300"},{"key":"27","doi-asserted-by":"publisher","DOI":"10.1145\/996841.996869"},{"key":"28","doi-asserted-by":"publisher","DOI":"10.1145\/1029894.1029911"},{"key":"3","doi-asserted-by":"crossref","first-page":"98","DOI":"10.1145\/1040305.1040314","article-title":"Synthesis of interface specifications for java classes","author":"alur","year":"2005","journal-title":"Proc POPL"},{"key":"2","year":"0","journal-title":"PolySpace Program Analysis Tool"},{"key":"10","first-page":"154","article-title":"Counterexampleguided abstraction refinement","author":"clarke","year":"2000","journal-title":"CAV"},{"key":"1","year":"0","journal-title":"Program Verifier"},{"key":"7","first-page":"35","article-title":"Slam2: Static driver verification with under 4% false alarms","author":"ball","year":"2010","journal-title":"FMCAD"},{"key":"6","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378846"},{"key":"5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73368-3_41"},{"key":"4","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503275"},{"key":"9","doi-asserted-by":"publisher","DOI":"10.1145\/781151.781153"},{"key":"8","first-page":"193","article-title":"Symbolic model checking without BDDs","author":"biere","year":"1999","journal-title":"TACAS"}],"event":{"name":"2011 26th IEEE\/ACM International Conference on Automated Software Engineering (ASE)","location":"Lawrence, KS, USA","start":{"date-parts":[[2011,11,6]]},"end":{"date-parts":[[2011,11,10]]}},"container-title":["2011 26th IEEE\/ACM International Conference on Automated Software Engineering (ASE 2011)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/6093623\/6100039\/06100046.pdf?arnumber=6100046","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,11]],"date-time":"2023-06-11T22:19:18Z","timestamp":1686521958000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/6100046\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,11]]},"references-count":28,"URL":"https:\/\/doi.org\/10.1109\/ase.2011.6100046","relation":{},"subject":[],"published":{"date-parts":[[2011,11]]}}}