{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T12:41:33Z","timestamp":1754484093171},"publisher-location":"Berlin, Heidelberg","reference-count":10,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540578260"},{"type":"electronic","value":"9783540483465"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-57826-9_142","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T13:26:17Z","timestamp":1330262777000},"page":"281-294","source":"Crossref","is-referenced-by-count":8,"title":["Implementing a methodology for formally verifying RISC processors in HOL"],"prefix":"10.1007","author":[{"given":"Sofi\u00e8ne","family":"Tahar","sequence":"first","affiliation":[]},{"given":"Ramayya","family":"Kumar","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"key":"22_CR1","doi-asserted-by":"crossref","unstructured":"Cohn, A.: A Proof of the Viper Microprocessor The First Level; In: VLSI Specification, Verification and Synthesis, Eds. G. Birtwistle and P.A. Subrahmanyam, Kluwer, 1988.","DOI":"10.1007\/978-1-4613-2007-4_2"},{"key":"22_CR2","volume-title":"Computer Architecture A Quantitative Approach","author":"J. Hennessy","year":"1990","unstructured":"Hennessy, J., Patterson, D.: Computer Architecture A Quantitative Approach; Morgan Kaufmann Publishers, Inc. San Mateo, California, 1990."},{"key":"22_CR3","unstructured":"Hunt, W.: The Mechanical Verification of a Microprocessor Design; In: From HDL Description to Guaranteed Correct Circuit Designs, Ed. D. Borrione, North-Holland, 1987."},{"key":"22_CR4","unstructured":"Joyce, J.: Multi-Level Verification of Microprocessor-Based Systems; PhD thesis, Cambridge University, December 1989."},{"key":"22_CR5","doi-asserted-by":"crossref","first-page":"165","DOI":"10.1007\/BF01383880","volume":"2","author":"R. Kumar","year":"1993","unstructured":"Kumar, R., Schneider, K., Kropf, Th.: Structuring and Automating Hardware Proofs in a Higher-Order Theorem-Proving Environment; Journal of Formal Methods in System Design, Vol. 2, pp. 165\u2013230, 1993.","journal-title":"Journal of Formal Methods in System Design"},{"key":"22_CR6","doi-asserted-by":"crossref","unstructured":"Melham, Th.:Abstraction Mechanisms for Hardware Verification; In: VLSI Specification, Verification and Synthesis, Eds. G. Birtwistle and P. A. Subrahmanyam, Kluwer, 1988.","DOI":"10.1007\/978-1-4613-2007-4_9"},{"key":"22_CR7","doi-asserted-by":"crossref","unstructured":"Srivas, M., Bickford, M.: Verification of a Pipelined Microprocessor Using Clio; In: Hardware Specification, Verification and Synthesis: Mathematical Aspects, Eds. M. Leeser and G. Brown, Springer, 1990.","DOI":"10.1007\/0-387-97226-9_35"},{"key":"22_CR8","volume-title":"Proc. of Euro-ARCH'93","author":"S. Tahar","year":"1993","unstructured":"Tahar, S., Kumar, R.: A Formalization of a Hierarchical Model for RISC Processors; to appear in Proc. of Euro-ARCH'93, Munich, Germany, Springer Verlag, 1993."},{"key":"22_CR9","volume-title":"Proc. of the 1993 International Conference on Computer Design","author":"S. Tahar","year":"1993","unstructured":"Tahar, S., Kumar, R.: Towards a Methodology for the Formal Hierarchical Verification of RISC Processors; to appear in Proc. of the 1993 International Conference on Computer Design, Cambridge, Massachusetts, IEEE, 1993."},{"key":"22_CR10","volume-title":"PhD thesis, University of California","author":"P. Windley","year":"1990","unstructured":"Windley, P.: The Formal Verification of Generic Interpreters; PhD thesis, University of California, Davis, Division of Computer Science, July 1990."}],"container-title":["Lecture Notes in Computer Science","Higher Order Logic Theorem Proving and Its Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-57826-9_142.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:14:28Z","timestamp":1605647668000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-57826-9_142"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540578260","9783540483465"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/3-540-57826-9_142","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}