{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:03:29Z","timestamp":1725663809282},"publisher-location":"Berlin, Heidelberg","reference-count":12,"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_141","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T13:26:16Z","timestamp":1330262776000},"page":"267-280","source":"Crossref","is-referenced-by-count":2,"title":["Abstraction techniques for modeling real-world interface chips"],"prefix":"10.1007","author":[{"given":"David A.","family":"Fura","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Phillip J.","family":"Windley","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Arun K.","family":"Somani","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"key":"21_CR1","unstructured":"S. Bainbridge, A. Camilleri, and R. Fleming, \u201cTheorem Proving as an Industrial Tool for System Level Design,\u201d in V. Stavridou, T.F. Melham, R.T. Boute (eds.). Theorem Provers in Circuit Design, Elsevier Science Publishers, 1992."},{"key":"21_CR2","unstructured":"D. A. Fura, P.J. Windley, and G.C. Cohen, \u201cTowards the Formal Specification of the Requirements and Design of a Processor Interface Unit,\u201d NASA Contractor Report 4521, 1993."},{"key":"21_CR3","unstructured":"M.J.C. Gordon, \u201cVerifying Real-Time Programs: A Case Study,\u201d in Hoare and Gordon (eds.), Mechanized Reasoning and Hardware Design, Prentice Hall, 1992."},{"key":"21_CR4","unstructured":"M.J.C. Gordon and T.F. Melham, Introduction to HOL: A Theorem Proving Environment for Higher Order Logic, Cambridge University Press, 1993."},{"key":"21_CR5","volume-title":"Ph.D. thesis and Institute for Computing Science Technical Report 47","author":"W.A. Hunt Jr.","year":"1986","unstructured":"W.A. Hunt Jr., FM8501: A Verified Microprocessor, Ph.D. thesis and Institute for Computing Science Technical Report 47, University of Texas at Austin, February 1986."},{"key":"21_CR6","unstructured":"Intel Corporation, 80960MC Hardware Designer's Reference Manual, 1989."},{"key":"21_CR7","unstructured":"J.J. Joyce, Multi-Level Verification of Microprocessor-Based Systems, Ph.D. thesis and Technical Report No. 195, Computer Laboratory, University of Cambridge, May 1990."},{"key":"21_CR8","unstructured":"G. Kane, MIPS R2000 RISC Architecture, Prentice Hall, 1987."},{"key":"21_CR9","unstructured":"T.F. Melham, Formalizing Abstraction Mechanisms for Hardware Verification in Higher Order Logic, Ph.D. thesis and Technical Report 201, University of Cambridge, August 1990."},{"key":"21_CR10","unstructured":"R. Milner, Communication and Concurrency, Prentice Hall, 1989."},{"key":"21_CR11","unstructured":"E.T. Schubert, \u201cVerification of Composed Hardware Systems Using CCS,\u201d in M. Archer, J. Joyce, K. Levitt, and P. Windley (eds.). Proceedings of the 1991 International Workshop on the HOL Theorem Proving System and its Applications, IEEE Computer Society Press, 1992."},{"key":"21_CR12","volume-title":"Ph.D. thesis and Research Report CSE-90-22","author":"P.J. Windley","year":"1990","unstructured":"P.J. Windley, The Formal Verification of Generic Interpreters, Ph.D. thesis and Research Report CSE-90-22, 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-57826-9_141.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,28]],"date-time":"2021-04-28T01:08:30Z","timestamp":1619572110000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-57826-9_141"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540578260","9783540483465"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/3-540-57826-9_141","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}