{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:09:52Z","timestamp":1725664192041},"publisher-location":"Berlin, Heidelberg","reference-count":42,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540612544"},{"type":"electronic","value":"9783540683896"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61254-8_30","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T16:20:21Z","timestamp":1330273221000},"page":"264-287","source":"Crossref","is-referenced-by-count":1,"title":["Abstraction of hardware construction"],"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,1]]},"reference":[{"unstructured":"D. A. Basin, G. M. Brown, and M. E. Leeser, Formally verified synthesis of combinational CMOS circuits. In L. J. M. Claesen, editor, Formal VLSI Specification and Synthesis, pages 197\u2013206, North-Holland, 1990.","key":"15_CR1"},{"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.","key":"15_CR2"},{"unstructured":"G. Birtwistle and B. Graham, Verifying the SECD in HOL. In [32].","key":"15_CR3"},{"volume-title":"VLSI Specification, Verification and Synthesis","year":"1988","unstructured":"G. Birtwistle and P. Subrahmanyam, eds., VLSI Specification, Verification and Synthesis, Kluwer Academic Publishers, Boston, 1988.","key":"15_CR4"},{"unstructured":"B. Bose and S. D. Johnson, DDD-FM9001: Derivation of a Verified Microprocessor. In [29].","key":"15_CR5"},{"doi-asserted-by":"crossref","unstructured":"H. Busch, Proof-based transformation of formal hardware models. In [22], pp. 271\u2013296.","key":"15_CR6","DOI":"10.1007\/978-1-4471-3544-9_15"},{"doi-asserted-by":"crossref","unstructured":"K. M. Chandy and J. Mishra, Parallel Program Design. A Foundation. Addison Wesley, 1988.","key":"15_CR7","DOI":"10.1007\/978-1-4613-9668-0_6"},{"volume-title":"IMEC-IFIP International Workshop on Applied Formal Methods for Correct VLSI Design, Volume 1+2","year":"1989","unstructured":"L. Claesen, editor, IMEC-IFIP International Workshop on Applied Formal Methods for Correct VLSI Design, Volume 1+2, Elsevier \/North-Holland, 1989.","key":"15_CR8"},{"key":"15_CR9","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":"A. Cohn, A Proof of Correctness of the Viper Microprocessor: First Level. In [4], pp. 27\u201371."},{"doi-asserted-by":"crossref","unstructured":"A. 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.","key":"15_CR10","DOI":"10.1007\/978-1-4612-3658-0_1"},{"unstructured":"M. P. Fourman, R. L. Harris, Lambda-Logic and Mathematics Behind Design Automation, 26th ACM\/IEEE Design Automation Conference, 1988.","key":"15_CR11"},{"unstructured":"M. P. Fourman, Formal System Design. In [32], pp 191\u2013236.","key":"15_CR12"},{"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":"15_CR13"},{"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":"15_CR14"},{"unstructured":"M. J. C. Gordon and T. F. Melham, Introduction to HOL. Cambridge University Press, 1993.","key":"15_CR15"},{"issue":"No.5","key":"15_CR16","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":"15_CR17","first-page":"532","volume-title":"IMEC-IFIP International Workshop on Applied Formal Methods for Correct VLSI Design, Volume 1+2","author":"F. K. Hanna","year":"1989","unstructured":"F. K. Hanna, M. Longley, and N. Daeche, Formal synthesis of digital systems. In [8], pages 532\u2013548."},{"doi-asserted-by":"crossref","unstructured":"F. K. Hanna and N. Daeche, Strongly-Typed Theory of Structure and Behaviors. In [29], pp. 39\u201354.","key":"15_CR18","DOI":"10.1007\/BFb0021713"},{"doi-asserted-by":"crossref","unstructured":"N. A. Harman and J. V. Tucker, Algebraic Models and the Correctness of Microprocessors. In [29], pp. 92\u2013108.","key":"15_CR19","DOI":"10.1007\/BFb0021717"},{"unstructured":"J. M. J. Herbert, Incremental Design and Formal Verification of Microcoded Microprocessors. In [34], pp. 157\u2013174.","key":"15_CR20"},{"key":"15_CR21","series-title":"Report","volume-title":"Ph.D. Thesis","author":"W. A. Hunt","year":"1985","unstructured":"W. A. Hunt, FM8501, A Verified Microprocessor. Ph.D. Thesis, Report No. 47, Institute for Computing Science, University of Texas, Austin, December 1985."},{"doi-asserted-by":"crossref","unstructured":"G. Jones and M. Sheeran, Designing Correct Circuits Springer, 1991.","key":"15_CR22","DOI":"10.1007\/978-1-4471-3544-9"},{"unstructured":"G. Jones and M. Sheeran, Circuit Design in Ruby. In [32].","key":"15_CR23"},{"unstructured":"J. J. Joyce, Multi-Level Verification of Microprocessor-Based Systems, Ph.D. Thesis, Computer Laboratory, Cambridge University, December 1989 (Technical Report No. 195, May 1990).","key":"15_CR24"},{"doi-asserted-by":"crossref","unstructured":"J. J. Joyce, Generic Specification of Digital Hardware. In [22], pp. 68\u201391.","key":"15_CR25","DOI":"10.1007\/978-1-4471-3544-9_4"},{"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":"15_CR26"},{"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":"15_CR27"},{"doi-asserted-by":"crossref","unstructured":"T. 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.","key":"15_CR28","DOI":"10.1007\/978-1-4613-2007-4_9"},{"doi-asserted-by":"crossref","unstructured":"G. J. Milne and L. Pierre, eds., Correct Hardware Design and Verification Methods, LNCS 683, Springer-Verlag, May 1993.","key":"15_CR29","DOI":"10.1007\/BFb0021709"},{"doi-asserted-by":"crossref","unstructured":"L. C. Paulson. Isabelle Tutorial and User's Manual, 1990.","key":"15_CR30","DOI":"10.2172\/10131497"},{"doi-asserted-by":"crossref","unstructured":"M. Srivas and M. Bickford, Formal Verification of a Pipelined Microprocessor, In IEEE Software, September 1990, pp. 52\u201364.","key":"15_CR31","DOI":"10.1109\/52.57892"},{"unstructured":"J. Staunstrup, editor, IFIP WG 10.5 Formal Methods for VLSI Design, North-Holland, 1990.","key":"15_CR32"},{"doi-asserted-by":"crossref","unstructured":"J. Staunstrup, A Formal Approach to Hardware Design. Kluwer Academic Publishers, 1994.","key":"15_CR33","DOI":"10.1007\/978-1-4615-2764-0"},{"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":"15_CR34"},{"key":"15_CR35","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."},{"doi-asserted-by":"crossref","unstructured":"S. Tahar and R. Kumar, Towards a Methodology for the Formal Verification of RISC Processors. In Proceedings IEEE International Conference on Computer Design (ICCD'93), 1993, pp. 58\u201362.","key":"15_CR36","DOI":"10.1109\/ICCD.1993.393405"},{"key":"15_CR37","first-page":"405","volume-title":"IMEC-IFIP International Workshop on Applied Formal Methods for Correct VLSI Design, Volume 1+2","author":"D. Verkest","year":"1989","unstructured":"D. Verkest and L. Claesen and H. De Man, On the use of the Boyer-Moore theorem prover for correctness proofs of parametrized hardware modules. In [8], pp. 405\u2013422."},{"unstructured":"Li-Guo Wang, Synthesis of Nondeterministic Logic Programs, Chinese Journal of Software, Vo. 1, No. 1, ISSN 1000-9825, CN 11-2560, January 1990.","key":"15_CR38"},{"unstructured":"Li-Guo Wang, Formal Derivation of A Class of Computers. PhD Thesis, LFCS, Department of Computer Science, University of Edinburgh, ECS-CST-119-95, September 1995.","key":"15_CR39"},{"doi-asserted-by":"crossref","unstructured":"Li-Guo Wang and M. Mendler, Formal Derivation of A Class of Computers: Its high stage \u2014 abstract microprogramming. In H. Eveking and P. Camurati, eds., Correct Hardware Design and Verification Methods (CHARME'95), Springer LNCS 987, 1995, pp. 84\u2013102.","key":"15_CR40","DOI":"10.1007\/3-540-60385-9_6"},{"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.","key":"15_CR41","DOI":"10.1109\/RISP.1990.63863"},{"doi-asserted-by":"crossref","unstructured":"P. J. Windley, A Theory of Generic Interpreters. In [29], pp. 122\u2013134.","key":"15_CR42","DOI":"10.1007\/BFb0021719"}],"container-title":["Lecture Notes in Computer Science","Higher-Order Algebra, Logic, and Term Rewriting"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61254-8_30.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T16:04:37Z","timestamp":1605629077000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61254-8_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540612544","9783540683896"],"references-count":42,"URL":"https:\/\/doi.org\/10.1007\/3-540-61254-8_30","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}