{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T00:08:43Z","timestamp":1725494923956},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540601609"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/3-540-49538-x_11","type":"book-chapter","created":{"date-parts":[[2007,11,11]],"date-time":"2007-11-11T03:37:18Z","timestamp":1194752238000},"page":"215-234","source":"Crossref","is-referenced-by-count":2,"title":["An Object-Oriented Framework for the Formal Verification of Processors"],"prefix":"10.1007","author":[{"given":"Laurent","family":"Arditi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"H\u00e9l\u00e8re","family":"Collavizza","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"11_CR1","unstructured":"F. Anceau. The Architecture of Microprocessors. Addison-Wesley Publishing Company, 1986."},{"key":"11_CR2","unstructured":"L. Arditi and H. Collavizza. Binary moment diagrams for verifying loops in microprocessor instructions. Technical report, Laboratoire I3S, Universit\u00e9 de Nice-Sophia Antipolis, Nov. 1994."},{"key":"11_CR3","unstructured":"L. Arditi and H. Collavizza. Towards verifying VHDL descriptions of processors. Technical report, Laboratoire I3S, Universit\u00e9 de Nice \u2014 Sophia Antipolis, Jan. 1995."},{"key":"11_CR4","volume-title":"The VHDL Cookbook","author":"P. J. Ashenden","year":"1990","unstructured":"P. J. Ashenden. The VHDL Cookbook. Public Domain, Dept. Computer Science, University of Adelaide, South Australia, first edition, July 1990.","edition":"first edition"},{"key":"11_CR5","doi-asserted-by":"crossref","unstructured":"G. Bracha and W. Cook. Mixin-based inheritance. In European Conference on Object Oriented Programming \/ Object-Oriented Programming Systems, Languages and Applications, October 1990.","DOI":"10.1145\/97945.97982"},{"key":"11_CR6","series-title":"Technical Report","volume-title":"Microprocessor verification: A tutorial","author":"M. L. Coe","year":"1992","unstructured":"M. L. Coe and P. J. Windley. Microprocessor verification: A tutorial. Technical Report LAL-92-10, Laboratory for Applied Logic, Brigham Young University, Provo, Utah, 1992."},{"key":"11_CR7","doi-asserted-by":"crossref","unstructured":"A. Colin. 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\u201371, Calgary, Canada, Jan. 1987. Kluwer Acad. Publishers.","DOI":"10.1007\/978-1-4613-2007-4_2"},{"key":"11_CR8","unstructured":"E. Gallesio. STklos: a Scheme object oriented system dealing with the TK toolkit. In Xhibition 94, San Jose, Jul. 1994. ICS."},{"key":"11_CR9","unstructured":"M. Gordon. HOL, a machine oriented formulation of higher order logic. Technical Report 68, University of Cambridge, Computer Laboratory, 1985."},{"issue":"2\/3","key":"11_CR10","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/BF00121125","volume":"1","author":"A. Gupta","year":"1992","unstructured":"A. Gupta. Formal hardware verification methods: a survey. Formal Methods in System Design, 1(2\/3):151\u2013238, Oct. 1992.","journal-title":"Formal Methods in System Design"},{"issue":"4","key":"11_CR11","doi-asserted-by":"publisher","first-page":"429","DOI":"10.1007\/BF00243132","volume":"5","author":"W. A. Hunt Jr","year":"1989","unstructured":"W. A. Hunt Jr. Microprocessor design verification. Journal of Automated Reasoning, 5(4):429\u2013460, Dec. 1989.","journal-title":"Journal of Automated Reasoning"},{"key":"11_CR12","doi-asserted-by":"crossref","unstructured":"J. J. Joyce. Formal verification and implementation of a microprocessor. In G. Birtwhistle and P. Subrahmanyam, editors, VLSI Specification, Verification and Synthesis, pages 129\u2013157, Calgary, Canada, Jan. 1987. Kluwer Acad. Publishers.","DOI":"10.1007\/978-1-4613-2007-4_4"},{"key":"11_CR13","unstructured":"B. Meyer. Object-Oriented Software Construction. Prentice Hall International, 1988."},{"key":"11_CR14","doi-asserted-by":"crossref","unstructured":"A. Paepcke. Object-oriented programming: the CLOS perspective. MIT press, 1993.","DOI":"10.7551\/mitpress\/5087.001.0001"},{"key":"11_CR15","series-title":"Technical Report","volume-title":"Microprocesseur \u00e0 test int\u00e9gr\u00e9 MTI \u2014 description fonctionnelle et architecture","author":"J. Pulou","year":"1987","unstructured":"J. Pulou, J. Rainard, and P. Thorel. Microprocesseur \u00e0 test int\u00e9gr\u00e9 MTI \u2014 description fonctionnelle et architecture. Technical Report NT\/CNS\/CC\/59, CNET, Grenoble, Jan. 1987."},{"key":"11_CR16","unstructured":"J. Rumbaugh, M. Blaha, W. Premerlani, F. Eddy, and W. Lorensen. Object-oriented Modeling and Design. Prentice Hall, 1991."},{"key":"11_CR17","unstructured":"R. Sekar and M. Srivas. Equational techniques. In G. Birtwistle and P. Subrahmanyam, editors, Current Trends in Hardware Verification and Automatic Theorem Proving, pages 173\u2013217, New-York, 1989. Springer-Verlag."},{"issue":"5","key":"11_CR18","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1109\/52.57892","volume":"7","author":"M. Srivas","year":"1990","unstructured":"M. Srivas and M. Bickford. Formal verification of a pipelined microprocessor. IEEE Software, 7(5):52\u201364, Sept. 1990.","journal-title":"IEEE Software"},{"key":"11_CR19","unstructured":"V. Stavridou. Formal Methods in Circuit Design. Number 37 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1993."},{"key":"11_CR20","unstructured":"G. L. Steele Jr. Common Lisp the Language. Digital Press, second edition, 1990."},{"key":"11_CR21","unstructured":"P. J. Windley. The Formal Verification of Generic Interpreters. PhD thesis, University of California, Division of Computer Science, 1990."},{"key":"11_CR22","series-title":"Lect Notes Comput Sci","first-page":"253","volume-title":"Higher Order Logic Theorem Proving and Its Applications. 6 th Int. Work. HUG\u201993","author":"Z. Zhu","year":"1993","unstructured":"Z. Zhu, J. Joyce, and C. Seger. Verification of the Tamarack-3 microprocessor in a hybrid verification environment. In J. J. Joyce and C.-J. H. Seger, editors, Higher Order Logic Theorem Proving and Its Applications. 6 th Int. Work. HUG\u201993, volume 780 of LNCS, pages 253\u2013266, Vancouver, Canada, Aug. 1993. Springer-Verlag."}],"container-title":["Lecture Notes in Computer Science","Object-Oriented Programming"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-49538-X_11.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,28]],"date-time":"2021-04-28T00:51:51Z","timestamp":1619571111000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-49538-X_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540601609"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/3-540-49538-x_11","relation":{},"subject":[]}}