{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,2]],"date-time":"2025-08-02T16:59:23Z","timestamp":1754153963310,"version":"3.41.2"},"reference-count":16,"publisher":"IEEE","license":[{"start":{"date-parts":[[2007,10,1]],"date-time":"2007-10-01T00:00:00Z","timestamp":1191196800000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2007,10,1]],"date-time":"2007-10-01T00:00:00Z","timestamp":1191196800000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2007,10]]},"DOI":"10.1109\/iccd.2007.4601875","type":"proceedings-article","created":{"date-parts":[[2008,8,21]],"date-time":"2008-08-21T11:14:39Z","timestamp":1219317279000},"page":"19-24","source":"Crossref","is-referenced-by-count":4,"title":["Bounded model checking of embedded software in wireless cognitive radio systems"],"prefix":"10.1109","author":[{"given":"Nannan","family":"He","sequence":"first","affiliation":[{"name":"Department of Electrical and Computer Engineering, Virginia Tech, Blacksburg, 24061 USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael S.","family":"Hsiao","sequence":"additional","affiliation":[{"name":"Department of Electrical and Computer Engineering, Virginia Tech, Blacksburg, 24061 USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1109\/ICCD.2005.77"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1145\/174675.177907"},{"key":"ref12","first-page":"121","article-title":"A Survey of Program Slicing Techniques","author":"tip","year":"1995","journal-title":"J Programming Languages"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71209-1_28"},{"key":"ref14","article-title":"Making the Most of BMC Counterexamples","author":"groce","year":"2004","journal-title":"BMC Workshop"},{"year":"0","key":"ref15"},{"journal-title":"A Methodology for a Verifiable Software Platform to Secure Software Defined and Cognitive Radios SDR","year":"2005","author":"rondeau","key":"ref16"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1145\/996566.996630"},{"key":"ref3","article-title":"Using Counterexample Guided Abstraction Refinement to Find Complex Bugs","author":"bjesse","year":"2004","journal-title":"Proc DATE"},{"key":"ref6","first-page":"385","article-title":"Modular Verification of Software Components in C","author":"chai","year":"2003","journal-title":"Proc of ICSE"},{"key":"ref5","article-title":"Behop: A symbolic model checker for Boolean programs","author":"ball","year":"2000","journal-title":"Proc SPIN"},{"key":"ref8","first-page":"168","article-title":"A tool for checking ANSI-C programs","author":"clarke","year":"2004","journal-title":"TACAS"},{"key":"ref7","first-page":"1205","article-title":"Disjunctive Image Computation for Embedded Software Verification","author":"wang","year":"2006","journal-title":"Proc DATE"},{"key":"ref2","article-title":"Automatic Abstraction Without Counterexample","author":"mcmillan","year":"2003","journal-title":"TACAS"},{"journal-title":"Model checking","year":"2000","author":"clarke","key":"ref1"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040334"}],"event":{"name":"2007 25th International Conference on Computer Design ICCD 2007","start":{"date-parts":[[2007,10,7]]},"location":"Lake Tahoe, CA, USA","end":{"date-parts":[[2007,10,10]]}},"container-title":["2007 25th International Conference on Computer Design"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/4591423\/4601871\/04601875.pdf?arnumber=4601875","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,23]],"date-time":"2025-07-23T18:35:39Z","timestamp":1753295739000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/4601875\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,10]]},"references-count":16,"URL":"https:\/\/doi.org\/10.1109\/iccd.2007.4601875","relation":{},"subject":[],"published":{"date-parts":[[2007,10]]}}}