{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:24:36Z","timestamp":1761596676920},"reference-count":55,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[1996,8,1]],"date-time":"1996-08-01T00:00:00Z","timestamp":838857600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[1996,8,1]],"date-time":"1996-08-01T00:00:00Z","timestamp":838857600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[1996,8]]},"DOI":"10.1007\/s002360050051","type":"journal-article","created":{"date-parts":[[2002,8,25]],"date-time":"2002-08-25T07:47:25Z","timestamp":1030261645000},"page":"421-456","source":"Crossref","is-referenced-by-count":13,"title":["Algebraic models of microprocessors architecture and organisation"],"prefix":"10.1007","volume":"33","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":"60330421236_CR1","volume-title":"The Architecture of Microprocessors","author":"F. Anceau","year":"1986","unstructured":"Anceau, F.: The Architecture of Microprocessors. New York: Addison-Wesley 1986"},{"key":"60330421236_CR2","first-page":"23","volume-title":"Computer Structures: Principles and Examples","author":"M. Barbacci","year":"1982","unstructured":"Barbacci, M.: An Introduction to ISPS In: Siewiorek, D.P., Bell, C.G., Newell, A. (eds.) Computer Structures: Principles and Examples, pp. 23\u201332. Tokyo, McGraw Hill 1982"},{"key":"60330421236_CR3","volume-title":"Computer Engineering: A DEC View of Hardware Systems Design","author":"C.G. Bell","year":"1978","unstructured":"Bell, C.G., Mudge, J.C., McNamara, J.E.: Computer Engineering: A DEC View of Hardware Systems Design. Belford, MA: Digital Press 1978"},{"key":"60330421236_CR4","first-page":"129","volume-title":"Formal Methods for VLSI Design","author":"G. Birtwistle","year":"1990","unstructured":"Birtwistle, G., Graham, B.: Verifying SECD in HOL. In: Staunstrup, J. (ed.) Formal Methods for VLSI Design, pp. 129\u2013177. Amsterdam: North-Holland 1990."},{"key":"60330421236_CR5","series-title":"683","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/BFb0021724","volume-title":"Correct Hardware Design and Verification Methods","author":"B. Bose","year":"1993","unstructured":"Bose, B., Johnson, S.D.: DDD-FM9001: Derivation of a verified microprocessor In: Milne, G., Pierre, L. (eds.), Correct Hardware Design and Verification Methods, pp. 191\u2013202. Lecture Notes in Computer Science 683. New York: Springer 1993"},{"key":"60330421236_CR6","volume-title":"A Computational Logic Handbook","author":"R.S. Boyer","year":"1988","unstructured":"Boyer, R.S., Moore, J.S.: A Computational Logic Handbook, New York: Academic Press 1988"},{"key":"60330421236_CR7","series-title":"683","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/BFb0021718","volume-title":"Correct Hardware Design and Verification Methods","author":"J. Chazarain","year":"1993","unstructured":"Chazarain, J., Collavizza, H.: Combining symbolic evaluation and object-oriented approach for verifying processor-like architectures at the RT level. In: Milne, G., Pierre, L. (eds.) Correct Hardware Design and Verification Methods, pp. 109\u2013121. Lecture Notes in Computer Science 683, New York: Springer 1993"},{"key":"60330421236_CR8","first-page":"27","volume-title":"VLSI Specification, Verification and Synthesis","author":"A. Cohn","year":"1987","unstructured":"Cohn, A.: A proof of correctness of the VIPER microprocessor: the first levels. In: Birtwistle, G., Subrahmanyam, P.A. VLSI Specification, Verification and Synthesis, pp. 27\u201372. Dordrecht: Kluwer Academic Publishers 1987"},{"key":"60330421236_CR9","doi-asserted-by":"crossref","unstructured":"Cohn, A., Gordon, M.: A mechanized proof of correctness of a simple counter. pp. 65\u201396. In: McEvoy, K., Tucker, J.V. (eds.), Theoretical Foundations for VLSI Design, Cambridge University Press Tracts in Theoretical Computer Science 10, 1990","DOI":"10.1017\/CBO9780511569838.004"},{"key":"60330421236_CR10","first-page":"1","volume-title":"VLSI Specification, Verification, and Synthesis","author":"W.J. Cullyer","year":"1987","unstructured":"Cullyer, W.J.: Implementing safety critical systems: the viper microprocessor. In: Birtwistle, G., Subrahmanyam, P.A., VLSI Specification, Verification, and Synthesis, pp. 1\u201326. Dordrecht: Kluwer Academic Publishers 1987"},{"issue":"3","key":"60330421236_CR11","first-page":"133","volume":"134 E","author":"W.J. Cullyer","year":"1987","unstructured":"Cullyer, W.J.: Application of formal methods to the VIPER microprocessor. IEE Proceedings, 134 E, 3, pp. 133\u2013141 (1987)","journal-title":"IEE Proceedings"},{"key":"60330421236_CR12","volume-title":"EATCS Monograph","author":"H. Ehrig","year":"1985","unstructured":"Ehrig, H., Mahr, B.: Fundamentals of Algebraic Specification I: Equations and Initial Semantics, EATCS Monograph Vol. 6. Berlin: Springer 1985"},{"key":"60330421236_CR13","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-349-21622-2","volume-title":"Microprogrammed Systems Design","author":"J.S. Florentin","year":"1991","unstructured":"Florentin, J.S.: Microprogrammed Systems Design. New York: Macmillan, 1991"},{"key":"60330421236_CR14","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1007\/BFb0015045","volume-title":"Algebraic Methods: Theory, Tools and Applications, Lecture Notes in Computer Science 394","author":"A. Geser","year":"1989","unstructured":"Geser, A. A Specification of the Intel 8085 Microprocessor: A Case Study. In: Wirsing, M., Bergstra, J.A. (eds.) Algebraic Methods: Theory, Tools and Applications, Lecture Notes in Computer Science 394, pp. 347\u2013402. Berlin: Springer 1989"},{"key":"60330421236_CR15","volume-title":"Technical Report SRI-CSL-88-9, Computer Science Laboratory","author":"J.A. Goguen","year":"1988","unstructured":"Goguen, J.A., Winkler, T.: Introducing OBJ3. Technical Report SRI-CSL-88-9, Computer Science Laboratory, SRI International, Menlo Park, CA, 1988"},{"key":"60330421236_CR16","unstructured":"Gordon, M.: LCF-LSM, a system for specifying and verifying hardware. Technical Report No. 41, Computer Laboratory, University of Cambridge, 1983"},{"key":"60330421236_CR17","unstructured":"Gordon, M.: Proving a Computer Correct with the LCF-LSM Hardware Verification System. Technical Report No. 42, Computer Laboratory, University of Cambridge, 1983"},{"key":"60330421236_CR18","first-page":"73","volume-title":"VLSI Specification, Verification and Synthesis","author":"M. Gordon","year":"1987","unstructured":"Gordon, M.: HOL: A proof generating system for higher-order logic. In: Birtwistle, G., Sub-rahmanyam, P.A. (eds.) VLSI Specification, Verification and Synthesis, pp. 73\u2013128. Dordrecht: Kluwer Academic Publishers, 1987"},{"key":"60330421236_CR19","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3576-8","volume-title":"The SECD Microprocessor: a Verification Case Study","author":"B. Graham","year":"1992","unstructured":"Graham, B.: The SECD Microprocessor: a Verification Case Study. Dordrecht: Kluwer, 1992"},{"key":"60330421236_CR20","doi-asserted-by":"crossref","first-page":"40","DOI":"10.1007\/0-387-97226-9_23","volume-title":"Hardware Specification, Verification and Synthesis: Mathematical Aspects, Lecture Notes in Computer Science 408","author":"B. Graham","year":"1990","unstructured":"Graham, B., Birtwistle, G.: Formalising the design of an SECD chip. In: Leeser, M., Brown, G., (eds.) Hardware Specification, Verification and Synthesis: Mathematical Aspects, Lecture Notes in Computer Science 408, pp. 40\u201366. New York: Springer 1990"},{"key":"60330421236_CR21","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/BFb0021713","volume-title":"Correct Hardware Design and Verification Methods, Lecture Notes in Computer Science 683","author":"K. Hanna","year":"1993","unstructured":"Hanna, K., Daeche, N.: Strongly-typed theory of structures and behaviours. In: Milne, G., Pierre, L., (eds.), Correct Hardware Design and Verification Methods, Lecture Notes in Computer Science 683, pp. 39\u201354. New York: Springer 1993"},{"key":"60330421236_CR22","unstructured":"Harman, N.A.: Formal specifications for digital systems. Ph.D. Thesis, School of Computer Studies, University of Leeds, 1989"},{"key":"60330421236_CR23","first-page":"375","volume-title":"The Fusion of Hardware Design and Verification","author":"N.A. Harman","year":"1988","unstructured":"Harman, N.A., Tucker, J.V.: Clocks, retimings, and the formal specification of a UART. In: Milne, G.J. (ed.), The Fusion of Hardware Design and Verification, pp. 375\u2013396. Amsterdam: North-Holland, 1988"},{"key":"60330421236_CR24","unstructured":"Harman, N.A., Tucker, J.V.: Formal specification and the design of verifiable computers. In: Proceedings of the 1988 UK IT Conference, pp. 500\u2013503, University College Swansea, IEE, 1988"},{"key":"60330421236_CR25","doi-asserted-by":"crossref","unstructured":"Harman, N.A., Tucker, J.V.: The formal specification of a digital correlator I: Abstract user specification. Theoretical Foundations for VLSI Design, In: McEvoy, K., Tucker, J.V. (eds.), Cambridge University Press Tracts in Theoretical Computer Science 10, pp. 161\u2013262 (1990)","DOI":"10.1017\/CBO9780511569838.008"},{"key":"60330421236_CR26","first-page":"273","volume-title":"Correct Hardware Design Methodologies","author":"N.A. Harman","year":"1992","unstructured":"Harman, N.A., Tucker, J.V.: Consistent refinements of specifications for digital systems. In: Prinetto, P., Camurati, P. (eds.), Correct Hardware Design Methodologies, pp. 273\u2013295. Amsterdam: North-Holland 1992"},{"key":"60330421236_CR27","unstructured":"Harman, N.A., Tucker, J.V.: Specification, design and verification of a simple computer. To appear in proceedings of 2nd Institute of Mathematics and its Applications Conference on Mathematics for Dependable Systems, Oxford University press, in press"},{"key":"60330421236_CR28","unstructured":"Harman, N.A., Tucker, J.V.: A model of timing abstraction for synchronous digital hardware. In preparation (1994)"},{"key":"60330421236_CR29","unstructured":"Hunt, W.A.: FM8501: A Verified Microprocessor, The University of Texas at Austin Institute for Computing Science technical report 47, 1986"},{"issue":"4","key":"60330421236_CR30","doi-asserted-by":"publisher","first-page":"429","DOI":"10.1007\/BF00243132","volume":"5","author":"W.A. Hunt","year":"1989","unstructured":"Hunt, W.A.: Microprocessor design verification. J. Automated Reasoning, 5 (4), pp. 429\u2013460 (1989)","journal-title":"J. Automated Reasoning"},{"key":"60330421236_CR31","volume-title":"Mechanized Reasoning in Hardware Design","author":"W. Hunt","year":"1992","unstructured":"Hunt, W., A formal, HDL and its use in the FM9001 verification. In: Hoare, C.A.R., Gordon, M. (eds.), Mechanized Reasoning in Hardware Design, Englewood Cliffs, NJ: Prentice-Hall 1992"},{"key":"60330421236_CR32","volume-title":"Lecture Notes in Artificial Intelligence 795","author":"W. Hunt","year":"1994","unstructured":"Hunt, W.: FM8501: A Verified Microprocessor, Lecture Notes in Artificial Intelligence 795, New York: Springer 1994"},{"key":"60330421236_CR33","volume-title":"Applied Formal Methods for Correct VLSI Design","author":"S.D. Johnson","year":"1991","unstructured":"Johnson, S.D., Zhu, Z.: An algebraic approach to hardware specification and derivation. In: Claesen, L. (eds), Applied Formal Methods for Correct VLSI Design, Amsterdam: Elsevier 1991"},{"key":"60330421236_CR34","first-page":"129","volume-title":"VLSI Specification, Verification and Synthesis","author":"J. Joyce","year":"1987","unstructured":"Joyce, J.: Formal verification and implementation of a microprocessor. In: Birtwistle, G., Sub-rahmanyam, P.A. (eds.), VLSI Specification, Verification and Synthesis, pp. 129\u2013159. Dordrecht: Kluwer Academic Publishers, 1987"},{"key":"60330421236_CR35","doi-asserted-by":"crossref","first-page":"308","DOI":"10.1093\/comjnl\/6.4.308","volume":"6","author":"P. Landin","year":"1963","unstructured":"Landin, P.: On the mechanical evaluation of expressions. Computer J., 6, 308\u2013320 1963","journal-title":"Computer J."},{"key":"60330421236_CR36","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1098\/rsta.1992.0022","volume":"339","author":"D. May","year":"1992","unstructured":"May, D., Barrett, G., Shepard, D.: Designing chips that work. Philos. Trans. Royal Soc. A 339, 3\u201319 1992","journal-title":"Philos. Trans. Royal Soc. A"},{"key":"60330421236_CR37","doi-asserted-by":"crossref","unstructured":"McEvoy, K., Tucker, J.V.: On theoretical foundations for hardware design. Theoretical Foundations for VLSI Design, In: McEvoy, K., Tucker, J.V. (eds.), pp. 1\u201364. Cambridge University Press Tracts in Theoretical Computer Science 10 (1990)","DOI":"10.1017\/CBO9780511569838.002"},{"key":"60330421236_CR38","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1093\/oso\/9780198537359.003.0003","volume-title":"Handbook of Logic in Computer Science","author":"K. Meinke","year":"1992","unstructured":"Meinke, K., Tucker, J.V.: Universal Algebra. In: Abramsky, S., Gabbay, D., Maibaum, T.S.E. (eds.), Handbook of Logic in Computer Science, pp. 189\u2013411. Oxford: Oxford University Press 1992"},{"key":"60330421236_CR39","first-page":"27","volume-title":"The Fusion of Hardware Design and Verification","author":"T. Melham","year":"1988","unstructured":"Melham T.: Using recursive types to reason about hardware in higher order logic. In: Milne, G.J. (ed.), The Fusion of Hardware Design and Verification, pp. 27\u201350. Amsterdam: North-Holland 1988"},{"key":"60330421236_CR40","doi-asserted-by":"crossref","unstructured":"Melham, T.F.: Higher Order Logic and Hardware Verification. Cambridge University Press Tracts in Theoretical Computer Science 31 (1993)","DOI":"10.1017\/CBO9780511569845"},{"key":"60330421236_CR41","volume-title":"Proc. Computer Hardware Description Languages and their Applications","author":"G.J. Milne","year":"1989","unstructured":"Milne, G.J.: Timing constraints: Formalising their description and verification. In: Proc. Computer Hardware Description Languages and their Applications, Amsterdam: North-Holland 1989"},{"key":"60330421236_CR42","unstructured":"Milne, G.J.: The formal description and verification of hardware timing. University of Strathclyde Computer Science Report HDV-8-90, 1990"},{"key":"60330421236_CR43","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1098\/rsta.1992.0030","volume":"339","author":"W. Roscoe","year":"1992","unstructured":"Roscoe, W.: Occam in the specification and verification of microprocessors. Philos. Trans. Royal Soc. A 339, 137\u2013151 (1992)","journal-title":"Philos. Trans. Royal Soc. A"},{"key":"60330421236_CR44","volume-title":"Computer Organisation and Architecture: Principles of Function and Structure","author":"W. Stallings","year":"1987","unstructured":"Stallings, W.: Computer Organisation and Architecture: Principles of Function and Structure. New York: Macmillan 1987"},{"key":"60330421236_CR45","unstructured":"Stavridou, V: Formal Specification of Digital Systems, Cambridge University Press Tracts in Theoretical Computer Science 37 (1993)"},{"key":"60330421236_CR46","first-page":"159","volume-title":"The Fusion of Hardware Design and Verification","author":"P.A. Subrahmanyam","year":"1988","unstructured":"Subrahmanyam, P.A.: Contextual constraints, temporal abstraction and observational equivalence in VLSI Design. In: Milne, G.J. (ed.), The Fusion of Hardware Design and Verification, pp. 159\u2013184. Amsterdam: North-Holland 1988"},{"key":"60330421236_CR47","unstructured":"Thompson, B.C., Tucker, J.V.: Equational specification of synchronous concurrent algebras and architectures. Department of Computer Science CSR 9.91, University College Swansea, 1991"},{"key":"60330421236_CR48","first-page":"1","volume-title":"Logic Algebra and Computation","author":"J.V. Tucker","year":"1991","unstructured":"Tucker, J.V.: Theorey of computation and specification over abstract data types and its applications. In: Bauer, F.L. (ed.), Logic Algebra and Computation, pp. 1\u201340. Berlin: Springer 1991"},{"key":"60330421236_CR49","volume-title":"Program Correctness over Abstract Data Types with Error State Semantics","author":"J.V. Tucker","year":"1988","unstructured":"Tucker, J.V., Zucker, J.I.: Program Correctness over Abstract Data Types with Error State Semantics. Amsterdam: North-Holland 1988"},{"key":"60330421236_CR50","unstructured":"Tucker, J.V., Zucker, J.I.: Generalised computability and algebraic specifications for abstract data types. In preparation (1999)"},{"key":"60330421236_CR51","volume-title":"EATCS Monograph","author":"W. Wechler","year":"1991","unstructured":"Wechler, W.: Universal algebra for computer scientists. EATCS Monograph, Berlin: Springer 1991"},{"key":"60330421236_CR52","doi-asserted-by":"crossref","unstructured":"Weijland, W.P.: Verification of a systolic algorithm in process algebra. Theoretical Foundations for VLSI Design, In: McEvoy, K., Tucker, J.V. (eds.), Cambridge University Press Tracts in Theoretical Computer Science 10 (1990)","DOI":"10.1017\/CBO9780511569838.006"},{"key":"60330421236_CR53","series-title":"683","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/BFb0021719","volume-title":"Correct Hardware Design and Verification Methods","author":"P. Windley","year":"1993","unstructured":"Windley, P.: A theorey of generic intepreters. In: Milne, G., Pierre, L. (eds.), Correct Hardware Design and Verification Methods, pp. 122\u2013134. Lecture Notes in Computer Science 683, Berlin: Springer 1993"},{"key":"60330421236_CR54","first-page":"675","volume-title":"Handbook of Theoretical Computer Science, Volume B: Formal Models and semantics","author":"M. Wirsing","year":"1990","unstructured":"Wirsing, M.: Algebraic specification. In: van Leeuwen, J. (ed.), Handbook of Theoretical Computer Science, Volume B: Formal Models and semantics, pp. 675\u2013788. Amsterdam: Elsevier 1990"},{"key":"60330421236_CR55","unstructured":"Zhu, A., Johnson, S.D.: An example of interactive hardware transformation. Indiana University, Computer Science Department (draft), 1991"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s002360050051.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s002360050051\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s002360050051","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s002360050051.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,12,30]],"date-time":"2023-12-30T06:46:12Z","timestamp":1703918772000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s002360050051"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996,8]]},"references-count":55,"journal-issue":{"issue":"5","published-print":{"date-parts":[[1996,8]]}},"alternative-id":["60330421236"],"URL":"https:\/\/doi.org\/10.1007\/s002360050051","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"value":"0001-5903","type":"print"},{"value":"1432-0525","type":"electronic"}],"subject":[],"published":{"date-parts":[[1996,8]]}}}