{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,15]],"date-time":"2025-08-15T00:29:38Z","timestamp":1755217778423,"version":"3.43.0"},"reference-count":29,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2001,5,1]],"date-time":"2001-05-01T00:00:00Z","timestamp":988675200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2001,5,1]],"date-time":"2001-05-01T00:00:00Z","timestamp":988675200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Formal Methods in System Design"],"published-print":{"date-parts":[[2001,5]]},"DOI":"10.1023\/a:1011217102270","type":"journal-article","created":{"date-parts":[[2002,12,23]],"date-time":"2002-12-23T04:18:21Z","timestamp":1040617101000},"page":"233-248","source":"Crossref","is-referenced-by-count":11,"title":["Efficient Simulation of Formal Processor Models"],"prefix":"10.1007","volume":"18","author":[{"given":"Matthew","family":"Wilding","sequence":"first","affiliation":[]},{"given":"David","family":"Greve","sequence":"additional","affiliation":[]},{"given":"David","family":"Hardin","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"322920_CR1","unstructured":"K.L. Albin, B.C. Brock, W.A. Hunt, Jr., and L.M. Smith, \u201cTesting the FM9001 microprocessor,\u201d Technical Report 90, Computational Logic, Inc., January 1995."},{"key":"322920_CR2","unstructured":"Averstar Inc. JWatch home page, 1998. 0http:\/ \/www.jwatch.com."},{"issue":"11","key":"322920_CR3","doi-asserted-by":"crossref","first-page":"1368","DOI":"10.1109\/32.41331","volume":"15","author":"W.R. Bevier","year":"1989","unstructured":"W.R. Bevier, \u201cKIT: A study in operating system verification,\u201d IEEE Transactions on Software Engineering, Vol. 15, No. 11, pp. 1368\u201381, 1989.","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"4","key":"322920_CR4","doi-asserted-by":"crossref","first-page":"411","DOI":"10.1007\/BF00243131","volume":"5","author":"W.R. Bevier","year":"1989","unstructured":"W.R. Bevier, W.A. Hunt, Jr., J.S. Moore, and W.D. Young, \u201cAn approach to systems verification,\u201d Journal of Automated Reasoning, Vol. 5, No. 4, pp. 411\u2013428, 1989.","journal-title":"Journal of Automated Reasoning"},{"key":"322920_CR5","volume-title":"Formal Methods in Computer-Aided Design\u2014FMCAD","author":"M. Bickford","year":"1996","unstructured":"M. Bickford and D. Jamsek, \u201cFormal specification and verification of VHDL,\u201d in M. Srivas and A. Camilleri (Eds.), Formal Methods in Computer-Aided Design\u2014FMCAD, Vol. 1166 of Lecture Notes in Computer Science, Springer-Verlag, Palo Alto, CA, 1996."},{"key":"322920_CR6","volume-title":"A Computational Logic Handbook","author":"R.S. Boyer","year":"1988","unstructured":"R.S. Boyer and J S Moore, A Computational Logic Handbook, Academic Press, Boston, 1988."},{"key":"322920_CR7","volume-title":"Automated Reasoning and Its Applications: Essays in Honor of Larry Wos.","author":"R.S. Boyer","year":"1996","unstructured":"R.S. Boyer and J S. Moore, \u201cMechanized formal reasoning about programs and computing machines,\u201d in R. Veroff (Ed.), Automated Reasoning and Its Applications: Essays in Honor of Larry Wos., MIT Press, Cambridge, MA, 1996."},{"issue":"1","key":"322920_CR8","doi-asserted-by":"crossref","first-page":"166","DOI":"10.1145\/227595.227603","volume":"43","author":"R.S. Boyer","year":"1996","unstructured":"R.S. Boyer and Y. Yu, \u201cAutomated proofs of object code for a widely used microprocessor,\u201d Journal of the ACM, Vol. 43, No. 1, pp. 166\u2013192, 1996.","journal-title":"Journal of the ACM"},{"key":"322920_CR9","unstructured":"B. Brock, ACL2 Integer Hardware Specification (IHS) Books, 1998. (available on ACL2 home page)."},{"key":"322920_CR10","volume-title":"Formal Methods in Computer-Aided Design\u2014FMCAD","author":"B. Brock","year":"1996","unstructured":"B. Brock, M. Kaufmann, and J.S. Moore, \u201cACL2 theorems about commercial microprocessors,\u201d in M. Srivas and A. Camilleri, (Eds.), Formal Methods in Computer-Aided Design\u2014FMCAD, vol. 1166 of Lecture Notes in Computer Science, Springer-Verlag, Palo Alto, CA, 1996."},{"issue":"1","key":"322920_CR11","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1023\/A:1008685826293","volume":"11","author":"B.C. Brock","year":"1997","unstructured":"B.C. Brock and W.A. Hunt, Jr., \u201cThe DUAL-EVAL hardware description language and its use in the formal specification and verification of the FM9001 microprocessor,\u201d Formal Methods in System Design, Vol. 11, No. 1. pp. 71\u2013104, July 1997.","journal-title":"Formal Methods in System Design"},{"key":"322920_CR12","unstructured":"D. Greve, M. Wilding, and D. Hardin, 1999 ACL2 Workshop Presentations, 1999, http:\/\/hokiepokie. org\/docs."},{"key":"322920_CR13","volume-title":"Formal Methods in Computer-Aided Design\u2014FMCAD","author":"D.A. Greve","year":"1998","unstructured":"D.A. Greve, \u201cSymbolic simulation of the JEM1 microprocessor,\u201d in Formal Methods in Computer-Aided Design\u2014FMCAD, Lecture Notes in Computer Science, Springer-Verlag, Palo Alto, CA, 1998."},{"key":"322920_CR14","unstructured":"D.A. Greve and M.M. Wilding, \u201cStack-based Java a back-to-future step,\u201d Electronic Engineering Times, p. 92, January 12, 1998."},{"key":"322920_CR15","volume-title":"C\u2014A Reference Manual","author":"S.P. Harbison","year":"1991","unstructured":"S.P. Harbison and G.L. Steele, Jr., C\u2014A Reference Manual, Prentice Hall, Upper Saddle River, NJ, 1991."},{"key":"322920_CR16","unstructured":"D. Hardin, D. Greve, M. Wilding, and J. Cowles, \u201cSingle-threaded formal processor models: Enabling proof and high-speed execution,\u201d Technical Report, Rockwell Collins Advanced Technology Center, Cedar Rapids, IA 52498, 1999, http:\/\/hokiepokie.org\/docs."},{"key":"322920_CR17","volume-title":"Computer-Aided Verification\u2014CAV '98","author":"D. Hardin","year":"1998","unstructured":"D. Hardin, M. Wilding, and D. Greve, \u201cTransforming the theorem prover into a digital design tool: From concept car to off-road vehicle,\u201d in A.J. Hu and M.Y. Vardi (Eds.), Computer-Aided Verification\u2014CAV '98, vol. 1427 of Lecture Notes in Computer Science, Springer-Verlag, Vancouver, Canada, 1998."},{"issue":"4","key":"322920_CR18","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1109\/32.588534","volume":"3","author":"M. Kaufmann","year":"1997","unstructured":"M. Kaufmann and J S. Moore, \u201cAn industrial strength theorem prover for a logic based on Common Lisp,\u201d E Transactions on Software Engineering Vol. 3, No. 4, pp. 203\u2013213, April 1997.","journal-title":"E Transactions on Software Engineering"},{"key":"322920_CR19","volume-title":"The Java Virtual Machine Specification","author":"T. Lindholm","year":"1996","unstructured":"T. Lindholm and F. Yellin, The Java Virtual Machine Specification, AddisonWesley, Reading, Massachusetts, 1996."},{"key":"322920_CR20","unstructured":"R.S. Boyer and J S. Moore, Single-Threaded Objects in ACL2, 1999, http:\/\/www.cs.utexas.edu\/users\/ moore\/publications."},{"key":"322920_CR21","series-title":"Technical Report","volume-title":"Formal verification of the AAMP-FV microcode","author":"S.P. Miller","year":"1996","unstructured":"S.P. Miller, D.A. Greve, M.M. Wilding, and M. Srivas, \u201cFormal verification of the AAMP-FV microcode,\u201d Technical Report, Rockwell Collins, Inc., Cedar Rapids, IA, 1996."},{"key":"322920_CR22","unstructured":"S.P. Miller and M. Srivas, \u201cFormal verification of the AAMP5 microprocessor: A case study in the industrial use of formal methods,\u201d in WIFT'95:Workshop on Industrial-Strength Formal Specification Techniques, Boca Raton, FL, 1995, IEEE Computer Society."},{"key":"322920_CR23","volume-title":"User Guide for the PVS Specification and Verification System (Beta Release)","author":"S. Owre","year":"1993","unstructured":"S. Owre, N. Shankar, and J.M. Rushby, User Guide for the PVS Specification and Verification System (Beta Release), Computer Science Laboratory, SRI International, Menlo Park, CA, February 1993."},{"key":"322920_CR24","volume-title":"PVS System Guide","author":"S. Owre","year":"1998","unstructured":"S. Owre, N. Shankar, J.M. Rushby, and D.W.J. Stringer-Calvert, PVS System Guide, Computer Science Laboratory, SRI International, Menlo Park, CA, September 1998."},{"key":"322920_CR25","unstructured":"Stephan Pfab, Personal communication, November 1997."},{"key":"322920_CR26","doi-asserted-by":"crossref","unstructured":"D.M. Russinoff, A mechanically checked proof of IEEE compliance of the floating point multiplication, division, and square root algorithms of the AMD-K7 processor, http:\/ \/www.onr.com\/user\/russ\/david. January 28, 1998.","DOI":"10.1112\/S1461157000000176"},{"key":"322920_CR27","volume-title":"Computer-Aided Verification\u2014CAV '93","author":"M. Wilding","year":"1993","unstructured":"M. Wilding, \u201cA mechanically verified application for a mechanically verified environment,\u201d in C. Courcoubetis (Ed.), Computer-Aided Verification\u2014CAV '93, vol. 697 of Lecture Notes in Computer Science. Springer-Verlag, Elounda, Greece, 1993."},{"key":"322920_CR28","unstructured":"M.M. Wilding, \u201cRobust computer system proofs in PVS,\u201d in C.M. Holloway and K.J. Hayhurst (Eds.), LFM97: Fourth NASA Langley Formal Methods Workshop, NASA Conference Publication no. 3356, Hampton, VA, 1997, http:\/\/atb-www.larc.nasa.gov\/Lfm97\/."},{"key":"322920_CR29","unstructured":"Alexander Wolfe, \u201cFirst Java-specific MPU rolls,\u201d Electronic Engineering Times, p. 1, September 22, 1997."}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1011217102270.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1011217102270\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1011217102270.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T19:07:04Z","timestamp":1754420824000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1011217102270"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001,5]]},"references-count":29,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2001,5]]}},"alternative-id":["322920"],"URL":"https:\/\/doi.org\/10.1023\/a:1011217102270","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2001,5]]}}}