{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,30]],"date-time":"2024-10-30T09:51:07Z","timestamp":1730281867059,"version":"3.28.0"},"reference-count":20,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011,7]]},"DOI":"10.1109\/memcod.2011.5970511","type":"proceedings-article","created":{"date-parts":[[2011,8,3]],"date-time":"2011-08-03T22:16:29Z","timestamp":1312409789000},"page":"61-71","source":"Crossref","is-referenced-by-count":5,"title":["Verification of microarchitectural refinements in rule-based systems"],"prefix":"10.1109","author":[{"given":"Nirav","family":"Dave","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Katelman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Myron","family":"King","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"family":"Arvind","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jose","family":"Meseguer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73368-3_52"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2004.833614"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.11.036"},{"key":"ref13","first-page":"142","article-title":"Modeling and verification of out-of-order microprocessors in UCLID","volume":"2517","author":"lahiri","year":"2002","journal-title":"FMCAD '02"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-39724-3_28"},{"key":"ref15","first-page":"110","article-title":"Verification of an implementation of tomasulo's algorithm by compositional model checking","author":"kenneth","year":"1998","journal-title":"Proceedings of the 10th International Conference on Computer Aided Verification CAV '98"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0058037"},{"article-title":"Computer Organization & Design: The Hardware\/Software Interface","year":"1997","author":"patterson","key":"ref17"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1007\/s11334-011-0149-0"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-85114-1_18"},{"article-title":"Bluespec SystemVerilog Version 3.8 Reference Guide","year":"2004","author":"waltham","key":"ref4"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68237-0_2"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1145\/800157.805047"},{"key":"ref5","first-page":"68","article-title":"Automatic verification of pipelined microprocessor control","author":"burch","year":"1994","journal-title":"Computer Aided Verification"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2010.5558626"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2007.371249"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1109\/40.768501"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2008.4547707"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2004.1382681"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1109\/12.368009"}],"event":{"name":"2011 9th IEEE\/ACM International Conference on Formal Methods and Models for Codesign (MEMOCODE 2011)","start":{"date-parts":[[2011,7,11]]},"location":"Cambridge","end":{"date-parts":[[2011,7,13]]}},"container-title":["Ninth ACM\/IEEE International Conference on Formal Methods and Models for Codesign (MEMPCODE2011)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/5959846\/5970502\/05970511.pdf?arnumber=5970511","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,25]],"date-time":"2019-06-25T15:35:07Z","timestamp":1561476907000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/5970511\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,7]]},"references-count":20,"URL":"https:\/\/doi.org\/10.1109\/memcod.2011.5970511","relation":{},"subject":[],"published":{"date-parts":[[2011,7]]}}}