{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,22]],"date-time":"2024-10-22T20:59:52Z","timestamp":1729630792630,"version":"3.28.0"},"reference-count":28,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1109\/memcod.2005.1487914","type":"proceedings-article","created":{"date-parts":[[2005,7,27]],"date-time":"2005-07-27T17:52:28Z","timestamp":1122486748000},"page":"188-197","source":"Crossref","is-referenced-by-count":8,"title":["A computationally ef~cient method based on commitment re~nement maps for verifying pipelined machines."],"prefix":"10.1109","author":[{"given":"P.","family":"Manolios","sequence":"first","affiliation":[]},{"given":"S.K.","family":"Srinivasan","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"19","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-35599-3_9"},{"key":"17","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":"LNCS"},{"journal-title":"Communication and Concurrency","year":"1990","author":"milner","key":"18"},{"key":"15","article-title":"Automatic verification of safety and liveness for XScale-like processor models using WEB-refinements","author":"manolios","year":"2004","journal-title":"Design Automation and Test in Europe DATE03"},{"key":"16","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2005.257"},{"journal-title":"Mechanical verification of reactive systems","year":"2001","author":"manolios","key":"13"},{"key":"14","first-page":"304","article-title":"A compositional theory of refinement for branching time","volume":"2860","author":"manolios","year":"2003","journal-title":"LNCS"},{"key":"11","first-page":"142","article-title":"Modeling and verification of out-of-order microprocessors using UCLID","volume":"2517","author":"lahiri","year":"2002","journal-title":"LNCS"},{"key":"12","first-page":"161","article-title":"Correctness of pipelined machines","volume":"1954","author":"manolios","year":"2000","journal-title":"LNCS"},{"key":"21","first-page":"284","article-title":"A simple characterization of stuttering bisimulation","volume":"1346","author":"namjoshi","year":"1997","journal-title":"LNCS"},{"key":"20","doi-asserted-by":"publisher","DOI":"10.1109\/DAC.2001.156196"},{"key":"22","doi-asserted-by":"publisher","DOI":"10.1109\/ICVD.1999.745161"},{"key":"23","first-page":"31","article-title":"Deductive verification of pipelined machines using first-order quantification","volume":"3114","author":"ray","year":"2004","journal-title":"LNCS"},{"journal-title":"Siege homepage","year":"0","author":"ryan","key":"24"},{"journal-title":"Formal verification of an advanced pipelined machine","year":"1999","author":"sawada","key":"25"},{"key":"26","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-3188-0_9"},{"key":"27","first-page":"135","article-title":"Processor verification with precise exceptions and speculative execution","volume":"1427","author":"sawada","year":"1998","journal-title":"LNCS"},{"key":"28","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2003.1210090"},{"key":"3","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(88)90098-9"},{"key":"2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30494-4_9"},{"journal-title":"ACL2 Homepage","year":"0","author":"kaufmann","key":"10"},{"key":"1","doi-asserted-by":"crossref","first-page":"433","DOI":"10.1007\/3-540-44798-9_33","article-title":"A framework for microprocessor correctness statements","volume":"2144","author":"aagaard","year":"2001","journal-title":"Lecture Notes in Computer Science"},{"key":"7","first-page":"208","article-title":"Assume-guarantee refinement between different time scales","volume":"1633","author":"henzinger","year":"1999","journal-title":"LNCS"},{"key":"6","first-page":"68","article-title":"Automatic verification of pipelined microprocessor control","volume":"818","author":"burch","year":"1994","journal-title":"LNCS"},{"key":"5","first-page":"78","article-title":"Modeling and verifying systems using a logic of counter arithmetic with lambda expressions and uninterpreted functions","volume":"2404","author":"bryant","year":"2002","journal-title":"LNCS"},{"key":"4","first-page":"470","article-title":"Exploiting positive equality in a logic of equality with uninterpreted functions","volume":"1633","author":"bryant","year":"0","journal-title":"LNCS"},{"journal-title":"Computer-Aided Reasoning An Approach","year":"2000","author":"kaufmann","key":"9"},{"key":"8","article-title":"Proof of correctness of a processor with reorder buffer using the completion functions approach","volume":"1633","author":"hosabettu","year":"1999","journal-title":"LNCS"}],"event":{"name":"Third ACM & amp; IEEE International Conference on Formal Methods and Models for Co-Design","acronym":"MEMCOD-05","location":"Verona, Italy"},"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\/01487914.pdf?arnumber=1487914","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,16]],"date-time":"2017-06-16T21:36:15Z","timestamp":1497648975000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/1487914\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"references-count":28,"URL":"https:\/\/doi.org\/10.1109\/memcod.2005.1487914","relation":{},"subject":[]}}