{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,12]],"date-time":"2026-03-12T01:08:12Z","timestamp":1773277692805,"version":"3.50.1"},"reference-count":17,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1109\/memcod.2005.1487887","type":"proceedings-article","created":{"date-parts":[[2005,7,27]],"date-time":"2005-07-27T13:52:28Z","timestamp":1122472348000},"page":"25-34","source":"Crossref","is-referenced-by-count":20,"title":["Automatic synthesis of cache-coherence protocol processors using Bluespec"],"prefix":"10.1109","author":[{"given":"N.","family":"Dave","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"M.C.","family":"Ng","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"family":"Arvind","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"17","doi-asserted-by":"publisher","DOI":"10.1145\/305138.305187"},{"key":"15","article-title":"Specification of memory models and design of provably correct cache coherence protocols","volume":"398","author":"shen","year":"1997","journal-title":"MIT CSAIL CSG Technical Memo"},{"key":"16","first-page":"47","article-title":"Proofs of correctness of cache-coherence protocols","author":"stoy","year":"2001","journal-title":"Proceedings of FME'01 Formal Methods for Increasing Software Productivity"},{"key":"13","first-page":"55","article-title":"Modular scheduling of guarded atomic actions","author":"rosenband","year":"2004","journal-title":"Proceedings 41st Design Automation Conference 2004 DAC"},{"key":"14","author":"shen","year":"2000","journal-title":"Design and Verification of Adaptive Cache Coherence Protocols"},{"key":"11","doi-asserted-by":"crossref","first-page":"300","DOI":"10.1007\/3-540-61474-5_78","article-title":"Protocol verification by aggregation of distributed transactions","author":"park","year":"1996","journal-title":"CAV '96 Proceedings of the 8th International Conference on Computer Aided Verification"},{"key":"12","doi-asserted-by":"publisher","DOI":"10.1109\/71.406955"},{"key":"3","year":"2004","journal-title":"Bluespec SystemVerilog Version 3 8 Reference Guide"},{"key":"2","doi-asserted-by":"publisher","DOI":"10.1109\/5.747867"},{"key":"1","article-title":"Cache-coherence verification with TLA+","author":"akhiani","year":"1999","journal-title":"World Congress on Formal Methods in the Development of Computing Systems Industrial Panel"},{"key":"10","article-title":"Deriving efficient cache coherence protocols through refi nement","author":"nalumasu","year":"0","journal-title":"Formal Methods for Parallel Programming Theory and Applications (FMPPTA)"},{"key":"7","doi-asserted-by":"publisher","DOI":"10.1109\/ISCA.1997.604691"},{"key":"6","author":"dave","year":"2005","journal-title":"Designing a processor in Bluespec"},{"key":"5","author":"culler","year":"1997","journal-title":"Modern Parallel Computer Architecture"},{"key":"4","doi-asserted-by":"publisher","DOI":"10.1145\/231379.231430"},{"key":"9","author":"lenoski","year":"1992","journal-title":"The Design and Analysis of DASH A Scalable Directorybased Multiprocessor"},{"key":"8","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2004.833614"}],"event":{"name":"Third ACM & amp; IEEE International Conference on Formal Methods and Models for Co-Design","location":"Verona, Italy","acronym":"MEMCOD-05"},"container-title":["Proceedings. Second ACM and IEEE International Conference on Formal Methods and Models for Co-Design, 2005. MEMOCODE '05."],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/9956\/32009\/01487887.pdf?arnumber=1487887","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,8]],"date-time":"2019-03-08T22:30:19Z","timestamp":1552084219000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/1487887\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"references-count":17,"URL":"https:\/\/doi.org\/10.1109\/memcod.2005.1487887","relation":{},"subject":[]}}