{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,25]],"date-time":"2025-09-25T18:16:14Z","timestamp":1758824174277},"publisher-location":"Berlin\/Heidelberg","reference-count":35,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"354056778X"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0021717","type":"book-chapter","created":{"date-parts":[[2005,11,23]],"date-time":"2005-11-23T09:47:42Z","timestamp":1132739262000},"page":"92-108","source":"Crossref","is-referenced-by-count":11,"title":["Algebraic models and the correctness of microprocessors"],"prefix":"10.1007","author":[{"given":"N. A.","family":"Harman","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J. V.","family":"Tucker","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"8_CR1","unstructured":"G Birtwistle and B Graham, \u201cVerifying SECD in HOL\u201d, pp.129\u2013177 in Formal Methods for VLSI Design, ed. J Staunstrup, North-Holland, (1990)."},{"key":"8_CR2","doi-asserted-by":"crossref","unstructured":"A Cohn and M Gordon, \u201cA Mechanised Proof of Correctness of a Simple Counter\u201d, pp.65\u201396 in Theoretical Foundations for VLSI Design, ed. K McEvoy and J V Tucker, Cambridge University Press, (1990).","DOI":"10.1017\/CBO9780511569838.004"},{"key":"8_CR3","unstructured":"A Cohn, \u201cA Proof of Correctness of the VIPER Microprocessor: the First Levels\u201d, pp.27\u201372 in VLSI Specification, Verification and Synthesis, ed. G Birtwistle and P A Subrahmanyam, Kluwer Academic Publishers, (1987)."},{"key":"8_CR4","unstructured":"W J Cullyer, \u201cImplementing Safety Critical Systems: the Viper Microprocessor\u201d, pp.1\u201326 in VLSI Specification, Verification, and Synthesis, ed. G Birtwistle and P A Subrahmanyam, Kluwer Academic Publishers, (1987)."},{"issue":"3","key":"8_CR5","first-page":"133","volume":"134 E","author":"W. J. Cullyer","year":"1987","unstructured":"W J Cullyer, \u201cApplication of Formal Methods to the VIPER Microprocessor\u201d, IEE Proceedings, 134 E, 3, pp.133\u2013141 (May 1987).","journal-title":"IEE Proceedings"},{"key":"8_CR6","doi-asserted-by":"crossref","unstructured":"J S Florentin, Microprogrammed Systems Design, Macmillan, (1991).","DOI":"10.1007\/978-1-349-21622-2"},{"key":"8_CR7","doi-asserted-by":"crossref","unstructured":"A Geser, \u201cA Specification of the Intel 8085 Microprocessor: A Case Study.\u201d, pp.347\u2013402 in Algebraic Methods: Theory, Tools and Applications, ed. M Wirsing and J A Bergstra, Lecture Notes in Computer Science 394, Springer-Verlag, (1989).","DOI":"10.1007\/BFb0015045"},{"key":"8_CR8","unstructured":"M Gordon, \u201cProving a Computer Correct with the LCF-LSM Hardware Verification System\u201d, Technical Report No. 42, Computer Laboratory, University of Cambridge, (1983)."},{"key":"8_CR9","unstructured":"M Gordon, \u201cHOL: A Proof Generating System for Higher-Order Logic\u201d, pp.73\u2013128 in VLSI Specification, Verification and Synthesis, ed. G Birtwistle and P A Subrahmanyam, Kluwer Academic Publishers, (1987)."},{"key":"8_CR10","doi-asserted-by":"crossref","unstructured":"B Graham and G Birtwistle, \u201cFormalising the Design of an SECD Chip\u201d, pp.40\u201366 in Hardware Specification, Verification and Synthesis: Mathematical Aspects, ed. M Leeser and G Brown, Lecture Notes in Computer Science 408, Springer Verlag, (1990).","DOI":"10.1007\/0-387-97226-9_23"},{"key":"8_CR11","doi-asserted-by":"crossref","unstructured":"B Graham, The SECD Microprocessor: a Verification Case Study, Kluwer, (1992).","DOI":"10.1007\/978-1-4615-3576-8"},{"key":"8_CR12","unstructured":"N A Harman and J V Tucker, \u201cClocks, Retimings, and the Formal Specification of a UART\u201d, pp.375\u2013396 in The Fusion of Hardware Design and Verification, ed. G J Milne, North-Holland, (1988)."},{"key":"8_CR13","unstructured":"N A Harman and J V Tucker, \u201cFormal Specification and the Design of Verifiable Computers\u201d, pp.500\u2013503 in Proceedings of the 1988 UK IT Conference, University College Swansea, IEE, (1988)."},{"key":"8_CR14","unstructured":"N A Harman and J V Tucker, \u201cThe Formal Specification of a Digital Correlator I: Abstract User Specification\u201d, pp.161\u2013262 in Theoretical Foundations for VLSI Design, ed. K McEvoy and J V Tucker, Cambridge University Press, (1990)."},{"key":"8_CR15","unstructured":"N A Harman and J V Tucker, \u201cConsistent Refinements of Specifications for Digital Systems\u201d, pp.273\u2013295 in Correct Hardware Design Methodologies, ed. P Prinetto and P Camurati, North-Holland, (1992)."},{"key":"8_CR16","unstructured":"N A Harman, \u201cFormal Specifications for Digital Systems\u201d, Ph.D. Thesis, School of Computer Studies, University of Leeds, (1989)."},{"key":"8_CR17","unstructured":"W A Hunt, \u201cFM8501: A Verified Microprocessor\u201d, The University of Texas at Austin Institute for Computing Science technical report 47, (1986)."},{"key":"8_CR18","unstructured":"S D Johnson and Z Zhu, \u201cAn Algebraic Approach to Hardware Specification and Derivation\u201d, in Proceedings of the IFIP International Workshop on Applied Formal Methods for Correct VLSI Design, ed. L Claesen, Elsevier, (1991)."},{"key":"8_CR19","doi-asserted-by":"crossref","unstructured":"J Joyce, \u201cFormal Verification and Implementation of a Microprocessor\u201d, pp.129\u2013159 in VLSI Specification, Verification and Synthesis, ed. G Birtwistle and P A Subrahmanyam, Kluwer Academic Publishers, (1987).","DOI":"10.1007\/978-1-4613-2007-4_4"},{"key":"8_CR20","unstructured":"P Landin, \u201cOn the Mechanical Evaluation of Expressions\u201d, Computer Journal, (1963)."},{"key":"8_CR21","doi-asserted-by":"crossref","unstructured":"K Meinke and J V Tucker, \u201cUniversal Algebra\u201d, pp.189\u2013411 in Handbook of Logic in Computer Science, ed. S Abramsky, D Gabbay, T S E Maibaum, Oxford University Press, (1992).","DOI":"10.1093\/oso\/9780198537359.003.0003"},{"key":"8_CR22","unstructured":"T Melham, \u201cUsing Recursive Types to Reason about Hardware in Higher Order Logic\u201d, pp.27\u201350 in The Fusion of Hardware Design and Verification, ed. G J Milne, North-Holland, (1988)."},{"key":"8_CR23","unstructured":"G J Milne, \u201cTiming Constraints: Formalising their Description and Verification\u201d, in Proceedings of Computer Hardware Description Languages and their Applications, North-Holland, (1989)."},{"key":"8_CR24","unstructured":"G J Milne, \u201cThe Formal Description and Verification of Hardware Timing\u201d, University of Strathclyde Computer Science Report HDV-8-90, (1990)."},{"key":"8_CR25","unstructured":"W Stallings, Computer Organisation and Architecture: Principles of Function and Structure, Macmillan, (1987)."},{"key":"8_CR26","unstructured":"V Stavridou, Formal Specification of Digital Systems, Cambridge Tracts in Theoretical Computer Science, CUP (in press), (1993)."},{"key":"8_CR27","unstructured":"P A Subrahmanyam, \u201cContextual Constraints, Temporal Abstraction and Observational Equivalence in VLSI Design\u201d, pp.159\u2013184 in The Fusion of Hardware Design and Verification, ed. G J Milne, North-Holland, (1988)."},{"key":"8_CR28","unstructured":"B C Thompson and J V Tucker, \u201cEquational Specification of Synchronous Concurrent Algebras and Architectures\u201d, Department of Computer Science CSR 9.91, University College Swansea, (1991)."},{"key":"8_CR29","unstructured":"J V Tucker and J I Zucker, Program Correctness over Abstract Data Types with Error State Semantics, North-Holland, (1988)."},{"key":"8_CR30","unstructured":"J V Tucker and J I Zucker, \u201cGeneralised Computability and Algebraic Specifications for Abstract Data Types\u201d, In preparation, (1993)."},{"key":"8_CR31","doi-asserted-by":"crossref","unstructured":"J V Tucker, \u201cTheory of Computation and Specification over Abstract Data Types and its Applications\u201d, in Logic, Algebra and Computation, ed. F L Bauer, Springer, (1991).","DOI":"10.1007\/978-3-642-76799-9_1"},{"key":"8_CR32","volume-title":"EATCS Monograph","author":"W Wechler","year":"1991","unstructured":"W Wechler, \u201cUniversal Algebra for Computer Scientists\u201d, EATCS Monograph, Springer-Verlag, Berlin, (1991)."},{"key":"8_CR33","doi-asserted-by":"crossref","unstructured":"W P Weijland, \u201cVerification of a Systolic Algorithm in Process Algebra\u201d, in Theoretical Foundations for VLSI Design, ed. K McEvoy and J V Tucker, Cambridge University Press, (1990).","DOI":"10.1017\/CBO9780511569838.006"},{"key":"8_CR34","doi-asserted-by":"crossref","unstructured":"M Wirsing, \u201cAlgebraic Specification\u201d, pp.675\u2013788 in Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics, ed. J van Leeuwen, Elsevier, (1990).","DOI":"10.1016\/B978-0-444-88074-1.50018-4"},{"key":"8_CR35","unstructured":"Z Zhu and S D Johnson, \u201cAn Example of Interactive Hardware Transformation\u201d, Indiana University, Computer Science Department (draft), (1991)."}],"container-title":["Lecture Notes in Computer Science","Correct Hardware Design and Verification Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/www.springerlink.com\/index\/pdf\/10.1007\/BFb0021717","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,1]],"date-time":"2024-02-01T02:29:04Z","timestamp":1706754544000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0021717"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["354056778X"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/bfb0021717","relation":{},"subject":[]}}