{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T12:15:47Z","timestamp":1754396147606,"version":"3.28.0"},"reference-count":22,"publisher":"IEEE Comput. Soc","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1109\/date.2004.1268844","type":"proceedings-article","created":{"date-parts":[[2004,6,21]],"date-time":"2004-06-21T17:52:40Z","timestamp":1087840360000},"page":"168-173","source":"Crossref","is-referenced-by-count":16,"title":["Automatic verification of safety and liveness for XScale-like processor models using WEB refinements"],"prefix":"10.1109","author":[{"given":"P.","family":"Manolios","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"S.K.","family":"Srinivasan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"19","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-3188-0_9"},{"key":"22","doi-asserted-by":"publisher","DOI":"10.1145\/337292.337331"},{"journal-title":"Siege homepage","year":"0","author":"ryan","key":"17"},{"journal-title":"Formal verification of an advanced pipelined machine","year":"1999","author":"sawada","key":"18"},{"key":"15","doi-asserted-by":"publisher","DOI":"10.1109\/DAC.2001.156196"},{"key":"16","doi-asserted-by":"publisher","DOI":"10.1109\/ICVD.1999.745161"},{"key":"13","first-page":"110","article-title":"Verification of an implementation of Tomasulo's algorithm by compositional model checking","volume":"1427","author":"mcmillan","year":"1998","journal-title":"CAV LNCS"},{"key":"14","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-35599-3_9"},{"journal-title":"Mechanical verification of reactive systems","year":"2001","author":"manolios","key":"11"},{"key":"12","first-page":"304","article-title":"A compositional theory of refinement for branching time","volume":"2860","author":"manolios","year":"2003","journal-title":"CHARME'03 of LNCS"},{"key":"21","doi-asserted-by":"publisher","DOI":"10.1109\/52.57892"},{"key":"3","first-page":"68","article-title":"Automatic verification of pipelined microprocessor control","volume":"818","author":"burch","year":"1994","journal-title":"CAV'94 of LNCS"},{"key":"20","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2003.1210090"},{"key":"2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45657-0_7"},{"key":"1","first-page":"470","article-title":"Exploiting positive equality in a logic of equality with uninterpreted functions","volume":"1633","author":"bryant","year":"1999","journal-title":"CA 99"},{"key":"10","first-page":"161","article-title":"Correctness of pipelined machines","volume":"1954","author":"manolios","year":"2000","journal-title":"Formal Methods in Computer-Aided Design Ser LNCS"},{"journal-title":"Computer-Aided Reasoning An Approach","year":"2000","author":"kaufmann","key":"7"},{"key":"6","doi-asserted-by":"publisher","DOI":"10.1145\/296333.296345"},{"key":"5","article-title":"Proof of correctness of a processor with reorder buffer using the completion functions approach","volume":"1633","author":"hosabettu","year":"1999","journal-title":"CAV LNCS"},{"key":"4","doi-asserted-by":"publisher","DOI":"10.1109\/4.962279"},{"key":"9","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1007\/3-540-36126-X_9","article-title":"Modeling and verification of out-of-order microprocessors using UCLID","volume":"2517","author":"lahiri","year":"2002","journal-title":"Formal Methods in Computer-Aided Design Ser LNCS"},{"journal-title":"ACL2 Homepage","year":"0","author":"kaufmann","key":"8"}],"event":{"name":". Design, Automation and Test in Europe Conference and Exhibition","acronym":"DATE-04","location":"Paris, France"},"container-title":["Proceedings Design, Automation and Test in Europe Conference and Exhibition"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/8959\/28390\/01268844.pdf?arnumber=1268844","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,16]],"date-time":"2017-06-16T04:12:14Z","timestamp":1497586334000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/1268844\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"references-count":22,"URL":"https:\/\/doi.org\/10.1109\/date.2004.1268844","relation":{},"subject":[]}}