{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:35:29Z","timestamp":1761597329930},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540590477"},{"type":"electronic","value":"9783540491774"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/3-540-59047-1_41","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T17:01:00Z","timestamp":1330275660000},"page":"33-51","source":"Crossref","is-referenced-by-count":17,"title":["A correctness model for pipelined microprocessors"],"prefix":"10.1007","author":[{"given":"Phillip J.","family":"Windley","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael L.","family":"Coe","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,1]]},"reference":[{"key":"3_CR1","doi-asserted-by":"crossref","unstructured":"Mark D. Aagaard and Miriam E. Leeser. Reasoning about pipelines with structural hazards. In Ramayya Kumar and Thomas Kropf, editors, Proceedings of the 1994 Conference on Theorem Provers in Circuit Design. Springer-Verlag, September 1994.","DOI":"10.1007\/3-540-59047-1_40"},{"key":"3_CR2","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1016\/0165-6074(87)90042-1","volume":"21","author":"J. P. Bowen","year":"1987","unstructured":"Jonathan P. Bowen. Formal specificaiton and documentation of microprocessor instruction sets. In Microprocessing and Microprogramming 21, pages 223\u2013230, 1987.","journal-title":"Microprocessing and Microprogramming"},{"key":"3_CR3","doi-asserted-by":"crossref","unstructured":"S. D. Crocker, E. Cohen, S. Landauer, and H. Orman. Reverification of a microprocessor. In Proceedings of the IEEE Symposium on Security and Privacy, pages 166\u2013176, April 1988.","DOI":"10.1109\/SECPRI.1988.8109"},{"key":"3_CR4","unstructured":"Albert Camilleri, Mike Gordon, and Tom Melham. Hardware verification using higher order logic. In D. Borrione, editor, From HDL Descriptions to Guaranteed Correct Circuit Designs. Elsevier Scientific Publishers, 1987."},{"key":"3_CR5","doi-asserted-by":"crossref","unstructured":"Alonzo Church. A formulation of the simple theory of types. Journal of Symbolic Logic, 5, 1940.","DOI":"10.2307\/2266170"},{"key":"3_CR6","doi-asserted-by":"crossref","unstructured":"Avra Cohn. A proof of correctness of the VIPER microprocessor: The first level. In G. Birtwhistle and P. Subrahmanyam, editors, VLSI Specification, Verification, and Synthesis, pages 27\u201372. Kluwer Academic Publishers, 1988.","DOI":"10.1007\/978-1-4613-2007-4_2"},{"key":"3_CR7","unstructured":"Michael J.C. Gordon. Proving a computer correct. Technical Report 41, Computer Lab, University of Cambridge, 1983."},{"key":"3_CR8","doi-asserted-by":"crossref","unstructured":"Michael J.C. Gordon. HOL: A proof generating system for higher-order logic. In G. Birtwhistle and P.A Subrahmanyam, editors, VLSI Specification, Verification, and Synthesis. Kluwer Academic Press, 1988.","DOI":"10.1007\/978-1-4613-2007-4_3"},{"key":"3_CR9","volume-title":"Theorem Provers in Circuit Design","author":"J. Herbert","year":"1992","unstructured":"John Herbert. Incremental design and formal verification of microcoded microprocessors. In V. Stavridou, T. F. Melham, and R. T. Boute, editors, Theorem Provers in Circuit Design, Proceedings of the IFIP WG 10.2 International Working Conference, Nijmegen, The Netherlands. North-Holland, June 1992."},{"key":"3_CR10","unstructured":"John L. Hennesy and David A. Patterson. Computer Architecture: A Quantitative Approach. Morgan Kaufmann Publishers Inc., 1990."},{"key":"3_CR11","doi-asserted-by":"crossref","first-page":"429","DOI":"10.1007\/BF00243132","volume":"5","author":"W. A. Hunt","year":"1989","unstructured":"Warren A. Hunt. Microprocessor design verification. Journal of Automated Reasoning, 5:429\u2013460, 1989.","journal-title":"Journal of Automated Reasoning"},{"key":"3_CR12","doi-asserted-by":"crossref","unstructured":"Jeffrey J. Joyce. Formal verification and implementation of a microprocessor. In G. Birtwhistle and P.A Subrahmanyam, editors, VLSI Specification, Verification, and Synthesis. Kluwer Academic Press, 1988.","DOI":"10.1007\/978-1-4613-2007-4_4"},{"key":"3_CR13","doi-asserted-by":"crossref","unstructured":"Thomas Melham. Abstraction mechanisms for hardware verification. In G. Birtwhistle and P. A. Subrahmanyam, editors, VLSI Specification, Verification and Synthesis. Kluwer Academic Publishers, 1988.","DOI":"10.1007\/978-1-4613-2007-4_9"},{"issue":"5","key":"3_CR14","doi-asserted-by":"crossref","first-page":"52","DOI":"10.1109\/52.57892","volume":"7","author":"M. Srivas","year":"1990","unstructured":"M. Srivas and M. Bickford. Formal verification of a pipelined microprocessor. IEEE Software, 7(5):52\u201364, September 1990.","journal-title":"IEEE Software"},{"key":"3_CR15","unstructured":"E. Thomas Schubert, Phillip J. Windley, and Karl Levitt. Report on the ucd microcoded viper verification project. In Jeffery J. Joyce and Carl Seger, editors, Proceedings of the 1993 International Workshop on the HOL Theorem Prover and its Applications., August 1993."},{"key":"3_CR16","doi-asserted-by":"crossref","unstructured":"Sofiene Tahar and Ramayya Kumar. Implementing a methodology for formally verifying RISC processors in HOL. In Jeffery J. Joyce and Carl Seger, editors, Proceedings of the 1993 International Workshop on the HOL Theorem Prover and its Applications., August 1993.","DOI":"10.1007\/3-540-57826-9_142"},{"key":"3_CR17","volume-title":"PhD thesis","author":"P. J. Windley","year":"1990","unstructured":"Phillip J. Windley., The Formal Verification of Generic Interpreters. PhD thesis, University of California, Davis, Division of Computer Science, June 1990."},{"key":"3_CR18","unstructured":"Phillip J. Windley. Using correctness results to verify behavioral properties of microprocessors. In Proceedings of the IEEE Computer Assurance Conference, June 1991."},{"key":"3_CR19","doi-asserted-by":"crossref","unstructured":"Phillip J. Windley. A theory of generic interpreters. In George J. Milne and Laurence Pierre, editors, Correct Hardware Design and Verification Methods, number 683 in Lecture Notes in Computer Science, pages 122\u2013134. Springer-Verlag, 1993.","DOI":"10.1007\/BFb0021709"},{"key":"3_CR20","unstructured":"Phillip J. Windley. Formal modeling and verification of microprocessors. IEEE Transactions on Computers, 1994. (to appear)."},{"key":"3_CR21","doi-asserted-by":"crossref","unstructured":"Phillip J. Windley. Specifying instruction set architectures in HOL: A primer. In Thomas Melham and Juanito Camilleri, editors, Proceedings of the 1994 International Workshop on the HOL Theorem Prover and its Applications. Springer Verlag, Spetember 1994.","DOI":"10.1007\/3-540-58450-1_59"}],"container-title":["Lecture Notes in Computer Science","Theorem Provers in Circuit Design"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-59047-1_41.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,28]],"date-time":"2021-04-28T01:22:22Z","timestamp":1619572942000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-59047-1_41"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540590477","9783540491774"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/3-540-59047-1_41","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}