{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:30:21Z","timestamp":1725456621179},"publisher-location":"Berlin\/Heidelberg","reference-count":16,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"354056778X"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0021719","type":"book-chapter","created":{"date-parts":[[2005,11,23]],"date-time":"2005-11-23T09:47:42Z","timestamp":1132739262000},"page":"122-134","source":"Crossref","is-referenced-by-count":11,"title":["A theory of generic interpreters"],"prefix":"10.1007","author":[{"given":"Phillip J.","family":"Windley","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"10_CR1","volume-title":"Master's thesis","author":"T. Arora","year":"1990","unstructured":"Tejkumar Arora. The formal verification of the VIPER microprocessor: EBM to microcode level. Master's thesis, University of California, Davis, 1990."},{"key":"10_CR2","unstructured":"Michael L. Coe and Phillip J. Windley. Using the Generic Interpreter Theory to Verify Microprocessors: A Tutorial. Technical Report LAL-92-10, University of Idaho, Department of Computer Science, Laboratory for Applied Logic. December, 1992."},{"key":"10_CR3","doi-asserted-by":"crossref","unstructured":"Avra Cohn. Correctness properties of the VIPER block model: The second level. Technical Report 134, University of Cambridge Computer Laboratory, May 1988.","DOI":"10.1007\/978-1-4612-3658-0_1"},{"key":"10_CR4","unstructured":"SRI International Computer Science Laboratory. EHDM Specification and Verification System: User's Guide, Version 4.1.1988."},{"key":"10_CR5","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":"10_CR6","unstructured":"J. Goguen and T. Winkler. Introducing OBJ3. Technical Report SRI-CSL-88-9, SRI International, August 1988."},{"key":"10_CR7","volume-title":"The Fusion of Hardware Design and Verification","author":"J. Herbert","year":"1988","unstructured":"John Herbert. Temporal abstraction of digital designs. In G.J. Milne, editor, The Fusion of Hardware Design and Verification, Proceedings of the IFIP WG 10.2 International Working Conference, Glasgow, Scotland. North-Holland, 1988."},{"key":"10_CR8","unstructured":"Warren A. Hunt. The mechanical verification of a microprocessor design. In D. Borrione, editor, From HDL Descriptions to Guaranteed Correct Circuit Designs. Elsevier Scientific Publishers, 1987."},{"key":"10_CR9","doi-asserted-by":"crossref","first-page":"429","DOI":"10.1007\/BF00243132","volume":"5","author":"A. H. Warren","year":"1989","unstructured":"Warren A. Hunt. Microprocessor design verification. Journal of Automated Reasoning, Vol 5, pages 429\u2013460,1989.","journal-title":"Journal of Automated Reasoning"},{"key":"10_CR10","unstructured":"Jeffrey J. Joyce. Multi-Level Verification of Microprocessor-Based Systems. PhD thesis, Cambridge University, December 1989."},{"key":"10_CR11","doi-asserted-by":"crossref","unstructured":"Paul Loewenstein. Reasoning about state machines in higher-order logic. In M. Leeser and G. Brown, editors, Workshop on Hardware Specification, Verification, and Synthesis: Mathematical Aspects, Lecture Notes in Computer Science. Springer-Verlag, 1989.","DOI":"10.1007\/0-387-97226-9_24"},{"key":"10_CR12","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"},{"key":"10_CR13","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":"10_CR14","doi-asserted-by":"crossref","unstructured":"Phillip J. Windley. A hierarchical methodology for the verification of microprogrammed microprocessors. In Proceedings of the IEEE Symposium on Security and Privacy, May 1990.","DOI":"10.1109\/RISP.1990.63863"},{"key":"10_CR15","unstructured":"Phillip J. Windley. The formal specification of a high-speed CMOS correlator. In Proceedings of the Third Annual IEEE\/NASA Symposium on VLSI Design, October 1991."},{"key":"10_CR16","doi-asserted-by":"crossref","unstructured":"Phillip J. Windley. Abstract Theories in HOL. In Proceedings of the 1992 International Conference on the HOL theorem Prover and its Application, October 1992.","DOI":"10.1016\/B978-0-444-89880-7.50019-X"}],"container-title":["Lecture Notes in Computer Science","Correct Hardware Design and Verification Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/www.springerlink.com\/index\/pdf\/10.1007\/BFb0021719","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,11]],"date-time":"2020-04-11T04:49:56Z","timestamp":1586580596000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0021719"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["354056778X"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/bfb0021719","relation":{},"subject":[]}}