{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T13:54:04Z","timestamp":1754488444002,"version":"3.40.2"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540584506"},{"type":"electronic","value":"9783540488033"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-58450-1_58","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T16:11:33Z","timestamp":1330272693000},"page":"424-439","source":"Crossref","is-referenced-by-count":3,"title":["Implementational issues for verifying RISC-pipeline conflicts 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,6,8]]},"reference":[{"key":"28_CR1","unstructured":"Anceau, F.: The Architecture of Microprocessors; Addison-Wesley Publishing Company, 1986."},{"key":"28_CR2","unstructured":"Buckow, O.: Formale Spezifikation und (Teil-) Verifikation eines SPARC-kompatiblen Prozessors mit LAMBDA; Diplomarbeit, Universit\u00e4t-Gesamthochschule Paderborn, Fachbereich Mathematik-Informatik, Oktober 1992."},{"key":"28_CR3","volume-title":"Electrical Engineering and Electronics","author":"S. Furber","year":"1989","unstructured":"Furber, S.: VLSI RISC Architecture and Organization; Electrical Engineering and Electronics, Dekker, New York, 1989."},{"key":"28_CR4","volume-title":"Introduction to HOL: A Theorem Proving Environment for Higher Order Logic","author":"M. Gordon","year":"1993","unstructured":"Gordon, M.; Melham, T.: Introduction to HOL: A Theorem Proving Environment for Higher Order Logic; Cambridge, University Press, 1993."},{"key":"28_CR5","unstructured":"Van De Goor, A.: Computer Architecture and Design; Addison-Wesley, 1989."},{"key":"28_CR6","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":"28_CR7","unstructured":"Joyce, J.: Multi-Level Verification of Microprocessor-Based Systems; Ph.D. Thesis, Computer Laboratory, Cambridge University, December 1989."},{"key":"28_CR8","unstructured":"Kogge, P.: The Architecture of Pipelined Computers; McGraw-Hill, 1981."},{"issue":"No.2","key":"28_CR9","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, No. 2, 1993, pp. 165\u2013230.","journal-title":"Journal of Formal Methods in System Design"},{"key":"28_CR10","unstructured":"Milutinovic, V.: High Level Language Computer Architecture; Computer Science Press, Inc., 1989."},{"key":"28_CR11","doi-asserted-by":"crossref","unstructured":"Srivas, M.; Bickford, M.: Formal Verification of a Pipelined Microprocessor; IEEE Software, September 1990, pp. 52\u201364.","DOI":"10.1109\/52.57892"},{"key":"28_CR12","unstructured":"Stone, H.: High-Performance Computer Architecture; Addison-Wesley Publishing Company, 1990."},{"key":"28_CR13","first-page":"591","volume-title":"A Formalization of a Hierarchical Model for RISC Processors","author":"S. Tahar","year":"1993","unstructured":"Tahar, S.; Kumar, R.: A Formalization of a Hierarchical Model for RISC Processors; In: Spies, P. (Ed.), Proc. European Informatics Congress Computing Systems Architecture (Euro-ARCH93), Munich, October 1993, Informatik Aktuell, Springer Verlag, pp. 591\u2013602."},{"key":"28_CR14","doi-asserted-by":"crossref","unstructured":"Tahar, S.; Kumar.R.: Towards a Methodology for the Formal Hierarchical Verification of RISC Processors; Proc. IEEE International Conference on Computer Design (ICCD93), Cambridge, Massachusetts, October 1993, pp. 58\u201362.","DOI":"10.1109\/ICCD.1993.393405"},{"key":"28_CR15","doi-asserted-by":"crossref","unstructured":"Tahar, S.; Kumar, R.: Implementing a Methodology for Formally Verifying RISC Processors in HOL; Proc. International Meeting on Higher Order Logic Theorem Proving and its Applications (HUG93), Vancouver, Canada, August 1993, pp. 283\u2013296.","DOI":"10.1007\/3-540-57826-9_142"},{"key":"28_CR16","unstructured":"Tahar, S.; Kumar, R.: Formal Verification of Pipeline Conflicts in RISC Processors; to appear in Proc. European Design Automation Conference (EURO-DAC94), Grenoble, France, September 1994."},{"key":"28_CR17","volume-title":"Ph.D. Thesis","author":"P. Windley","year":"1990","unstructured":"Windley, P.: The Formal Verification of Generic Interpreters; Ph.D. Thesis, Division of Computer Science, University of California, Davis, 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-58450-1_58.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T22:30:38Z","timestamp":1742596238000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-58450-1_58"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540584506","9783540488033"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/3-540-58450-1_58","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}