{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T13:31:27Z","timestamp":1754487087239},"publisher-location":"Berlin, Heidelberg","reference-count":39,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540603856"},{"type":"electronic","value":"9783540455165"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/3-540-60385-9_6","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T18:24:07Z","timestamp":1330280647000},"page":"84-102","source":"Crossref","is-referenced-by-count":3,"title":["Formal design of a class of computers \u2014 its high stage: abstract microprogramming"],"prefix":"10.1007","author":[{"given":"Li -Guo","family":"Wang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Mendler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"key":"6_CR1","unstructured":"Simon Bainbridge, Albert Camilleri and Roger Fleming, Theorem Proving as an Industrial Tool for System Level Design. In [34], pp. 253\u2013276."},{"key":"6_CR2","unstructured":"David A. Basin, Geoffrey M. Brown, and Miriam E. Leeser, Formally verified synthesis of combinational CMOS circuits. In L. J. M. Claesen, editor, Formal VLSI Specification and Synthesis, page 197\u2013206, North-Holland, 1990."},{"key":"6_CR3","unstructured":"D. A. Basin, Extracting Circuits from Constructive Proofs. In 1991 International Workshop on Formal Verification in VLSI Design. ACM IFIP WG 10.2, Jan. 1991."},{"volume-title":"VLSI Specification, Verification and Synthesis","year":"1988","key":"6_CR4","unstructured":"G. Birtwistle and P. Subrahmanyam, eds., VLSI Specification, Verification and Synthesis, Kluwer Academic Publishers, Boston, 1988."},{"key":"6_CR5","unstructured":"J. Bormann, H. Nusser-Wehlan, and G. Venzl, Formal Design in an Industrial Research Laboratory: Lessons and Perspectives. In J. Staunstrup and R. Sharp, eds., Designing Correct Circuits, North-Holland, 1992."},{"key":"6_CR6","unstructured":"D. Borrione, H. Collavizza and C. Le Faou, \u039cSPEED: A Framework for Specifying and Verifying Microprocessors. In Formal Methods in VLSI Design, Springer, 1991."},{"key":"6_CR7","unstructured":"B. Bose and S. D. Johnson, DDD-FM9001: Derivation of a Verified Microprocessor. In [30]."},{"key":"6_CR8","doi-asserted-by":"crossref","unstructured":"K. M. Chandy and J. Mishra, Parallel Program Design. A Foundation. Addison Wesley, 1988.","DOI":"10.1007\/978-1-4613-9668-0_6"},{"volume-title":"IMEC-IFIP International Workshop on Applied Formal Methods for Correct VLSI Design","year":"1989","key":"6_CR9","unstructured":"L. Claesen, editor, IMEC-IFIP International Workshop on Applied Formal Methods for Correct VLSI Design, Volume 1+2, Elsevier\/North-Holland, 1989."},{"key":"6_CR10","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1007\/978-1-4613-2007-4_2","volume-title":"VLSI Specification, Verification and Synthesis","author":"A. Cohn","year":"1988","unstructured":"Avra Cohn, A Proof of Correctness of the Viper Microprocessor: First Level. In [4], pp. 27\u201371."},{"key":"6_CR11","doi-asserted-by":"crossref","unstructured":"Avra Cohn, Correctness Properties of the Viper Block Model: The Second Level. In G. Birtwistle and P. Subrahmanyam, eds., Current Trends in Hardware Verification and Automated Theorem Proving, Springer-Verlag, 1989, pp.1\u201391.","DOI":"10.1007\/978-1-4612-3658-0_1"},{"key":"6_CR12","unstructured":"M. P. Fourman, R. L. Harris, Lambda-Logic and Mathematics Behind Design Automation, 26th ACD\/IEEE Design Automation Conference, 1988."},{"key":"6_CR13","unstructured":"M. P. Fourman, Formal System Design. In [33], pp 191\u2013236."},{"issue":"No.2","key":"6_CR14","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1145\/151244.151245","volume":"11","author":"G. Genesh","year":"1993","unstructured":"Gopalakrishnan, Genesh and Fujimoto, Richard, Design and Verification of the Rollback Chip Using HOP: a Case Study of Formal Methods Applied to Hardware Design. ACM Transactions on Computer Systems, Vo. 11 No. 2 pp. 109\u2013145, May 1993.","journal-title":"ACM Transactions on Computer Systems"},{"key":"6_CR15","unstructured":"M. J. C. Gordon, Proving a Computer Correct with the LCF-LSM Hardware Verification System. Technical Report No. 42, Computer Laboratory, University of Cambridge, 1983."},{"key":"6_CR16","unstructured":"M. J. C. Gordon, Why higher-order logic is a good formalism for specifying and verifying hardware. in: G. Milne and P. Subrahmanyam, eds., Formal Aspects of VLSI Design, North-Holland, 1986, pp. 153\u2013177."},{"key":"6_CR17","doi-asserted-by":"crossref","unstructured":"M. J. C. Gordon, HOL: A Proof Generating System for Higher-Order Logic. University of Cambridge, Computer Laboratory, Tech Report No. 103, 1987.","DOI":"10.1007\/978-1-4613-2007-4_3"},{"issue":"No.5","key":"6_CR18","first-page":"242","volume":"133","author":"F.K. Hanna","year":"1986","unstructured":"F.K. Hanna and N.Daeche, Specification and Verification of Digital Systems using Higher-Order Predicate Logic. IEE Proceedings, Vol. 133, Part E, No. 5, September 1986, pp. 242\u2013254.","journal-title":"IEE Proceedings"},{"key":"6_CR19","unstructured":"F.K. Hanna, M. Longley, and N. Daeche, Formal synthesis of digital systems. In [9], pages 532\u2013548."},{"key":"6_CR20","doi-asserted-by":"crossref","unstructured":"F.K. Hanna and N.Daeche. Strongly-Typed Theory of Structure and Behaviors. In [30], pp. 39\u201354.","DOI":"10.1007\/BFb0021713"},{"key":"6_CR21","doi-asserted-by":"crossref","unstructured":"N.A. Harman and J. V. Tucker, Algebraic Models and the Correctness of Microprocessors. In [30], pp. 92\u2013108.","DOI":"10.1007\/BFb0021717"},{"key":"6_CR22","volume-title":"Ph.D. Thesis, Report No. 47","author":"W. A. Hunt","year":"1985","unstructured":"Warren A. Hunt, FM8501, A Verified Microprocessor. Ph.D. Thesis, Report No. 47, Institute for Computing Science, University of Texas, Austin, December 1985."},{"key":"6_CR23","unstructured":"P.B. Jackson, Nuprl and its Use in Circuit Design. In [34], pp. 311\u2013336."},{"key":"6_CR24","unstructured":"G. Jones and M. Sheeran, Circuit Design in Ruby. In [33]."},{"key":"6_CR25","unstructured":"M. Langevin and E. Cerny, Verification of Processor-like Circuits. In Advanced Work on. Correct Hardware Design Methodology, Turin, 12\u201314 June 1991."},{"key":"6_CR26","unstructured":"J. J. Joyce, G. Birtwistle and M. Gordon, Proving a Computer Correct in Higher Order Logic. Report No. 100, Computer Laboratory, Cambridge University, 1986."},{"key":"6_CR27","unstructured":"Mahmood, M. and Mavaddat, F. and Elmasry, M.I. and Cheng, M.H.M, A Formal Language Model of Logic Microcode Synthesis. In [9], pp. 21\u201339."},{"key":"6_CR28","doi-asserted-by":"crossref","unstructured":"Thomas F. Melham, Abstraction mechanism for hardware verification. In G. Birtwistle and P.A. Subrahmanyam, eds., VLSI Specification, Verification, and Synthesis, pages 267\u2013291. Kluwer Academic Publishers, 1988.","DOI":"10.1007\/978-1-4613-2007-4_9"},{"key":"6_CR29","volume-title":"Hardware Specification, Verification and Synthesis: Mathematical Aspects","author":"G. J. Milne","year":"1989","unstructured":"G. J. Milne, Design for Verifiability. In Hardware Specification, Verification and Synthesis: Mathematical Aspects, Cornell University, USA, July 1989."},{"key":"6_CR30","doi-asserted-by":"crossref","unstructured":"G. J. Milne and L. Pierre, eds., Correct Hardware Design and Verification Methods, LNCS 683, Springer-Verlag, May 1993.","DOI":"10.1007\/BFb0021709"},{"key":"6_CR31","unstructured":"Lawrence C. Paulson. Isabelle Tutorial and User's Manual, 1990."},{"key":"6_CR32","doi-asserted-by":"crossref","unstructured":"J. Staunstrup, A Formal Approach to Hardware Design. Kluwer Academic Publishers, 1994.","DOI":"10.1007\/978-1-4615-2764-0"},{"key":"6_CR33","unstructured":"J. Staunstrup, editor, IFIP WG 10.5 Formal Methods for VLSI Design, North-Holland, 1990."},{"key":"6_CR34","unstructured":"V. Stavridou, T.F. Melham, and R.T. Boute, eds., Theorem Provers in Circuit Design: Theory, Practice and Experience. IFIP TC10\/WG 10.2, North Holland, June 1992."},{"key":"6_CR35","unstructured":"V. Stavridou, J. A. Goguen, A. Stevens, S. M. Eker, S. N. Alonefits, and K. M. Hobley, FUNNEL and 2OBJ: Towards and Integrated Hardware Design Environment. In [34]."},{"key":"6_CR36","first-page":"29","volume-title":"Designing Correct Circuits","author":"D. Suk","year":"1990","unstructured":"Dany Suk, Hardware Synthesis in Constructive Type Theory. In G. Jones and M. Sheeran, eds., Designing Correct Circuits, pp 29\u201349, Oxford, Springer-Verlag, 1990."},{"key":"6_CR37","doi-asserted-by":"crossref","first-page":"449","DOI":"10.1016\/B978-0-444-89880-7.50034-6","volume-title":"Higher Order Logic Theorem Proving and its Application","author":"L. Wang","year":"1993","unstructured":"Li-Guo Wang, Deriving a Correct Computer. In L. J. M. Claesen and M. J. C. Gordon, eds., Higher Order Logic Theorem Proving and its Application, pages 449\u2013458, Elsevier\/North-Holland, 1993."},{"key":"6_CR38","unstructured":"Li-Guo Wang, Formal Derivation of A Class of Computers. PhD Thesis, LFCS, Department of Computer Science, University of Edinburgh, Oct. 1994."},{"key":"6_CR39","doi-asserted-by":"crossref","unstructured":"P. J. Windley, A Hierarchical Methodology for the Verification of Microprogrammed Microprocessors. In IEEE Symposium on Security and Privacy, May 1990.","DOI":"10.1109\/RISP.1990.63863"}],"container-title":["Lecture Notes in Computer Science","Correct Hardware Design and Verification Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-60385-9_6.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:58:56Z","timestamp":1605646736000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-60385-9_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540603856","9783540455165"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/3-540-60385-9_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}