{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,8]],"date-time":"2026-05-08T16:13:17Z","timestamp":1778256797459,"version":"3.51.4"},"reference-count":25,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011,11]]},"DOI":"10.1109\/ase.2011.6100048","type":"proceedings-article","created":{"date-parts":[[2011,12,16]],"date-time":"2011-12-16T13:30:08Z","timestamp":1324042208000},"page":"143-152","source":"Crossref","is-referenced-by-count":10,"title":["Formalizing hardware\/software interface specifications"],"prefix":"10.1109","author":[{"given":"Juncao","family":"Li","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fei","family":"Xie","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Ball","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vladimir","family":"Levin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Con","family":"McGarvey","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"19","year":"2006","journal-title":"PIO-24 LPCI User Manual"},{"key":"17","author":"solomon","year":"1998","journal-title":"Inside Windows NT"},{"key":"18","year":"2005","journal-title":"IEEE Standard for Verilog (IEEE Std 1364-2005)"},{"key":"15","doi-asserted-by":"publisher","DOI":"10.1145\/1217935.1217943"},{"key":"16","article-title":"Context-bounded model checking of concurrent software","author":"qadeer","year":"0","journal-title":"Proc of TACAS 2005"},{"key":"13","doi-asserted-by":"publisher","DOI":"10.1145\/349214.349241"},{"key":"14","article-title":"COSPAN","author":"hardin","year":"0","journal-title":"Proc of CAV 1996"},{"key":"11","year":"2010"},{"key":"12","author":"schwoon","year":"2002","journal-title":"Model-checking Pushdown Systems"},{"key":"21","article-title":"Device simulation framework","year":"2010","journal-title":"MSDN"},{"key":"20","article-title":"Model checking bu?chi pushdown systems","author":"li","year":"0","journal-title":"Proc of FASE 2011"},{"key":"22","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0023719"},{"key":"23","article-title":"Equivalence checking of static affine programs using widening to handle recurrences","author":"verdoolaege","year":"0","journal-title":"Proc of CAV 2009"},{"key":"24","year":"2000","journal-title":"Universal Serial Bus Specification Revision 2 0"},{"key":"25","article-title":"Framework usb reference","year":"2010","journal-title":"MSDN"},{"key":"3","year":"2006","journal-title":"Intel 8255x 10\/100 Mbps Ethernet Controller Family - Open Source Software Developer Manual Version 1 3"},{"key":"2","doi-asserted-by":"publisher","DOI":"10.1145\/1289927.1289937"},{"key":"10","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2005.1487900"},{"key":"1","article-title":"Testing closed-source binary device drivers with DDT","author":"kuznetsov","year":"0","journal-title":"USENIX Annual Technical Conference 2010"},{"key":"7","doi-asserted-by":"publisher","DOI":"10.1145\/41840.41852"},{"key":"6","article-title":"Efficient Reachability Analysis of Bu?chi Pushdown Systems for Hardware\/Software Co-verification","author":"li","year":"0","journal-title":"Proc of CAV 2010"},{"key":"5","author":"li","year":"2010","journal-title":"An Automata-Theoretic Approach to Hardware\/Software Coverification"},{"key":"4","author":"kurshan","year":"1994","journal-title":"Computer-Aided Verification of Coordinating Processes The Automata-Theoretic Approach"},{"key":"9","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2009.09.043"},{"key":"8","article-title":"Interface automata","author":"de alfaro","year":"0","journal-title":"Proc of ESEC\/FSE 2001"}],"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\/06100048.pdf?arnumber=6100048","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,3,21]],"date-time":"2017-03-21T09:12:27Z","timestamp":1490087547000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/6100048\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,11]]},"references-count":25,"URL":"https:\/\/doi.org\/10.1109\/ase.2011.6100048","relation":{},"subject":[],"published":{"date-parts":[[2011,11]]}}}