{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,8]],"date-time":"2026-05-08T00:06:35Z","timestamp":1778198795920,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":42,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540627173","type":"print"},{"value":"9783540684909","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/bfb0027289","type":"book-chapter","created":{"date-parts":[[2005,11,19]],"date-time":"2005-11-19T07:00:45Z","timestamp":1132383645000},"page":"149-187","source":"Crossref","is-referenced-by-count":11,"title":["A practical method for rigorously controllable hardware design"],"prefix":"10.1007","author":[{"given":"E.","family":"B\u00f6rger","sequence":"first","affiliation":[]},{"given":"S.","family":"Mazzanti","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,17]]},"reference":[{"key":"10_CR1","doi-asserted-by":"crossref","unstructured":"M.Aagaard and M.Leeser. Reasoning About Pipelines with Structural Hazards, Springer LNCS 901, 1995.","DOI":"10.1007\/3-540-59047-1_40"},{"key":"10_CR2","unstructured":"W. Ahrendt. Von PROLOG zur WAM, Verifikation der Prozedur\u00fcbersetzung mit KIV. Diploma thesis, University of Karlsruhe, December 1995, pp.115."},{"key":"10_CR3","first-page":"239","volume":"780","author":"T. Arora","year":"1994","unstructured":"T.Arora, T.Leung, K.Levitt, T.Schubert, and P.Windley: Report on the UCD microcoded Viper verification project. Springer LNCS 780, 1994, 239\u2013252.","journal-title":"Springer LNCS"},{"key":"10_CR4","unstructured":"D.L.Beatty. A Methodology for Formal Hardware Verification, with Application to Microprocessors. PhD thesis, School of CS, CMU, Aug. 1993."},{"key":"10_CR5","doi-asserted-by":"crossref","unstructured":"E. B\u00f6rger. Why use evolving algebras for hardware and software engineering. in: M. Bartosek, J. Staudek, J. Wiedermann (Eds), SOFSEM'95, Springer LNCS 1012, 1995, 236\u2013271.","DOI":"10.1007\/3-540-60609-2_12"},{"key":"10_CR6","first-page":"145","volume-title":"A formal method for provably correct composition of a real-life processor out of basic components (The APE100 reverse engineering project)","author":"E. B\u00f6rger","year":"1995","unstructured":"E. B\u00f6rger and G. Del Castillo. A formal method for provably correct composition of a real-life processor out of basic components (The APE100 reverse engineering project). In: Proc. First IEEE International Conference Engineering of Complex Computer Systems (ICECCS'96). IEEE Comp. Soc. Press, Los Alamitos CA, 1995, 145\u2013148."},{"key":"10_CR7","doi-asserted-by":"crossref","first-page":"52","DOI":"10.1093\/comjnl\/39.1.52","volume":"39","author":"E. B\u00f6rger","year":"1996","unstructured":"E. B\u00f6rger and I. Durdanovi\u0107. Correctness of Compiling Occam to Transputer Code. in: Computer Journal 39, 1996, 52\u201392.","journal-title":"Computer Journal"},{"key":"10_CR8","unstructured":"E. B\u00f6rger and S. Mazzzanti. A Correctness Proof for Pipelinening in RISC Architectures DIMACS Technical Report 96-22, July 1996, pp.60."},{"key":"10_CR9","unstructured":"E. B\u00f6rger and D. Rosenzweig. The WAM \u2014 Definition and Compiler Correctness. in: Logic Programming: Formal Methods and Practical Applications (C.Beierle, L.Pl\u00fcmer, Eds.), Elsevier Science, 1995, 20\u201390 (chapter 2)."},{"key":"10_CR10","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1016\/0165-6074(87)90042-1","volume":"21","author":"J.P. Bowen","year":"1987","unstructured":"J.P.Bowen. Formal specifacation and documentation of microprocessor instruction sets. In: Microprocessing and Microprogramming 21, 223\u2013230, 1987.","journal-title":"Microprocessing and Microprogramming"},{"key":"10_CR11","volume-title":"Formale Spezifikation und Verifikation eines SPARC-kompatiblen Prozessors mit einem interaktiven Beweissystem","author":"O. Buckow","year":"1993","unstructured":"O. Buckow and J. Bormann. Formale Spezifikation und Verifikation eines SPARC-kompatiblen Prozessors mit einem interaktiven Beweissystem, Siemens Research and Development, M\u00fcnchen 1993."},{"key":"10_CR12","doi-asserted-by":"crossref","unstructured":"J.R. Burch and D.L.Dill. Automatic verification of pipelined microprocessor control. Conf. on Computer-Aided Verification, 1994.","DOI":"10.1007\/3-540-58179-0_44"},{"key":"10_CR13","doi-asserted-by":"crossref","unstructured":"J.A. Cohn. A proof of correctness of the VIPER microprocessor: The first level. In G.Birtwhistle and P.Subrahmanyam, editors, VLSI Specification, Verification, and Synthesis, pages 27\u201372. Kluwer Academic Publisher, 1988.","DOI":"10.1007\/978-1-4613-2007-4_2"},{"key":"10_CR14","doi-asserted-by":"crossref","unstructured":"J.A. Cohn. Correctness properties of the Viper block model: The second level. In: G.Birtwistle, editor, Proceedings of the 1988 Design Verification Conference. Springer-Verlag, 1989.","DOI":"10.1007\/978-1-4612-3658-0_1"},{"key":"10_CR15","unstructured":"D.Cyrluk. Microprocessor verification in PVS: A methodology and simple example. Technical Report SRI-CSL-93-12, SRI CS Lab, 1993."},{"key":"10_CR16","unstructured":"D.Cyrluk. A PVS specification, implementation and verification of DLX. SRI, Palo Alto (Oral Communication)."},{"key":"10_CR17","unstructured":"M. Dehof. Formale Spezifikation und Verifikation des DLX-RISC-Prozessors. Diploma Thesis, Inst. f. Technik der Informationsverarbeitung, University of Karlsruhe, August 1994."},{"key":"10_CR18","volume-title":"Technical Report No. SBF 358-C2-9\/94","author":"M. Dehof","year":"1994","unstructured":"M. Dehof and S. Tahar. Implementierung des DLX-RISC-Prozessors in einer Standardezellen-Entwurfsumgebung, Technical Report No. SBF 358-C2-9\/94, Institute of Computer Design and Fault Tolerance, University of Karlsruhe, Germany, March 1994."},{"key":"10_CR19","unstructured":"Y. Gurevich. Evolving Algebras 1993: Lipari Guide. In: Specification and validation methods, Ed. E. B\u00f6rger, Oxford University Press, 1995."},{"key":"10_CR20","doi-asserted-by":"crossref","unstructured":"E. Harcourt, J.Mauney, and T.Cook. From processor timing specifications to static instruction scheduling. In Static Analysis Symposium, September 1994.","DOI":"10.1007\/3-540-58485-4_36"},{"key":"10_CR21","unstructured":"J.L. Hennessy. Designing a computer as a microprocessor: Experience and lessons from the MIPS 4000. A lecture at the Symposium on Integrated Systems, Seattle, Washington, March, 1993."},{"key":"10_CR22","unstructured":"J.L. Hennessy and D.A. Patterson. Computer Architecture: a Quantitative Approach Morgan Kaufman Publisher, 1990. Revised second edition 1996."},{"key":"10_CR23","volume-title":"Incremental design and formal verification of microcoded microprocessor","author":"J. Herbert","year":"1992","unstructured":"J. Herbert. Incremental design and formal verification of microcoded microprocessor. In V. Stavridou, T.F. Melham, and R.T. Boute, editors, Theorem Provers in Cicruit Design, Proocedings of the IFIP WG 10.2 International Working Conference, Nijmegen, The Netherlands. North-Holland, June 1992."},{"key":"10_CR24","unstructured":"J.Huggins. Kermit: specification and verification. In: Specification and validation methods, Ed. E. B\u00f6rger, Oxford University Press, 1995."},{"key":"10_CR25","doi-asserted-by":"crossref","first-page":"429","DOI":"10.1007\/BF00243132","volume":"5","author":"W.A. Hunt","year":"1989","unstructured":"W.A. Hunt. Microprocessor design verification. Journal of Automated Reasoning, 5:429\u2013460, 1989.","journal-title":"Journal of Automated Reasoning"},{"key":"10_CR26","doi-asserted-by":"crossref","unstructured":"J.Joyce. Formal verification and implementation of a microprocessor. In: G.Birtwhistle and P.A.Subrahmanyan (Eds), VLSI specification, verification, and synthesis. Kluwer Ac. Press 1988.","DOI":"10.1007\/978-1-4613-2007-4_4"},{"key":"10_CR27","unstructured":"J.Joyce. Multi-level verification of microprocessor-based systems. PhD thesis, Cambridge Dec. 89."},{"key":"10_CR28","unstructured":"J.Joyce, G.Birtwistle, and M.Gordon. Proving a computer correct in higher order logic. TR 100, Computer Lab., University of Cambridge, 1986."},{"key":"10_CR29","doi-asserted-by":"crossref","first-page":"690","DOI":"10.1109\/TC.1979.1675439","volume":"C-28","author":"L. Lamport","year":"1979","unstructured":"L.Lamport. How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. on Computers, 1979, C-28, 690\u2013691.","journal-title":"IEEE Trans. on Computers"},{"key":"10_CR30","unstructured":"M.Langevin and E.Cerny. Verification of processor-like circuits. In: P.Prinetto and P.Camurati (Eds), Advanced research Workshop on Correct Hardware Dwsign Methodologies, June 1991."},{"key":"10_CR31","volume-title":"LNCS 1125","author":"C. Pusch","year":"1996","unstructured":"C.Pusch. Verification of Compiler Correctness for the WAM. In: Proc. Theorem Proving in Higher Order Logics (TPHOL'97, Turku), Springer LNCS 1125, 1996."},{"issue":"1652","key":"10_CR32","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1098\/rsta.1992.0030","volume":"339","author":"A.W. Roscoe","year":"1992","unstructured":"A.W.Roscoe. Occam in the specification and verification of microprocessors. Philosophical Transactions of the Royal Society of London, Series A: Physical Sciences and Engineering, 339(1652): 137\u2013151, Apr.15, 1992.","journal-title":"Philosophical Transactions of the Royal Society of London, Series A: Physical Sciences and Engineering"},{"key":"10_CR33","unstructured":"J.B.Saxe, S.J.Garland, J.V.Guttag and J.J.Horning. Using transformations and verification in circuit design. TR 78, DEC System Res. Center, 1991."},{"issue":"5","key":"10_CR34","doi-asserted-by":"crossref","first-page":"52","DOI":"10.1109\/52.57892","volume":"7","author":"M. Srivas","year":"1990","unstructured":"M. Srivas and M. Bickford. Formal verification af a pipelined microprocessor. IEEE Software, 7(5):52\u201364, September 1990.","journal-title":"IEEE Software"},{"key":"10_CR35","first-page":"XIV+162","volume-title":"Fortschrittberichte VDI, Reihe 10: Informatik\/Kommunikationstechnik Nr. 350","author":"S. Tahar","year":"1995","unstructured":"S.Tahar. Eine Methode zur formalen Verifikation von RISC-Prozessoren. Fortschrittberichte VDI, Reihe 10: Informatik\/Kommunikationstechnik Nr. 350, VDI-Verlag, D\u00fcsseldorf 1995, pp.XIV+162."},{"key":"10_CR36","doi-asserted-by":"crossref","unstructured":"S.Tahar and R.Kumar. Towards a methodology for the formal hierarchical verification of RISC processors. Proc. IEEE Int.Conf. on Computer Design (ICCD93), Cambridge\/Mass; Oct.1993, pp. 58\u201362.","DOI":"10.1109\/ICCD.1993.393405"},{"key":"10_CR37","first-page":"424","volume":"859","author":"S. Tahar","year":"1994","unstructured":"S.Tahar and R.Kumar. Implementational issues for verifying RISC-pipeline conflicts in HOL. Springer LNCS 859, 1994, pp. 424\u2013439.","journal-title":"Springer LNCS"},{"key":"10_CR38","unstructured":"S. Tahar and R.Kumar. A practical methodology for the formal verification of RISC processors. FZI TR Sept. 95, Karlsruhe, pp. iii+46."},{"key":"10_CR39","doi-asserted-by":"crossref","unstructured":"P.J.Windley. A hierarchical methodology for verifying microprogrammed mircoprocessors. Proc. IEEE Symp. on Security and Privacy, Oakland, May 1990, pp. 345\u2013357.","DOI":"10.1109\/RISP.1990.63863"},{"key":"10_CR40","unstructured":"P.J. Windley. Formal modelling and verification of microprocessors. IEEE Transactions on Computers, 1994."},{"key":"10_CR41","first-page":"440","volume":"859","author":"P.J. Windley","year":"1994","unstructured":"P.J. Windley. Specifying instruction-set architecture in HOL: a primer. Springer LNCS 859, 1994, pp. 440\u2013455.","journal-title":"Springer LNCS"},{"key":"10_CR42","unstructured":"P.J. Windley and M.L. Coe. A Correctness Model for Pipelined Microprocessors. Springer LNCS 901."}],"container-title":["Lecture Notes in Computer Science","ZUM '97: The Z Formal Specification Notation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0027289","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,11]],"date-time":"2020-04-11T01:32:05Z","timestamp":1586568725000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0027289"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540627173","9783540684909"],"references-count":42,"URL":"https:\/\/doi.org\/10.1007\/bfb0027289","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1997]]}}}