{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T12:03:21Z","timestamp":1754481801998},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540651918"},{"type":"electronic","value":"9783540495192"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/3-540-49519-3_21","type":"book-chapter","created":{"date-parts":[[2007,10,20]],"date-time":"2007-10-20T06:37:12Z","timestamp":1192862232000},"page":"321-333","source":"Crossref","is-referenced-by-count":27,"title":["Symbolic Simulation of the JEM1 Microprocessor"],"prefix":"10.1007","author":[{"given":"David A.","family":"Greve","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,5,17]]},"reference":[{"key":"21_CR1","series-title":"Technical report","volume-title":"SELECT-a formal system for testing and debugging programs by symbolic execution","author":"R. S. Boyer","year":"1975","unstructured":"Robert S. Boyer, Bernard Elspas, and Karl N. Levitt. SELECT-a formal system for testing and debugging programs by symbolic execution. Technical report, Stanford Research Institute, Menlo Park, CA, 1975. CSL-20."},{"key":"21_CR2","volume-title":"The Java Language Specification","author":"J. Gosling","year":"1996","unstructured":"James Gosling, Bill Joy, and Guy Steele. The Java Language Specification, Addison Wesley, Reading, Massachusetts, 1996."},{"key":"21_CR3","unstructured":"David Greve, Matthew Wilding, and David Hardin. Efficient simulation using a simple formal processor model. Technical report, Rockwell Collins Advanced Technology Center, April 1998. available at: \n                  http:\/\/home.plutonium.net\/~hokie\/docs\/efm.ps\n                  \n                ."},{"key":"21_CR4","unstructured":"David A. Greve and Matthew M. Wilding. Stack-based Java a back-to-future step. Electronic Engineering Times, page 92, January 12, 1998."},{"key":"21_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0031806","volume-title":"Formal Methods in Computer-Aided Design-FMCAD","author":"R. B. Jones","year":"1996","unstructured":"Robert B. Jones, Carl-Johan H. Seger, and David L. Dill. Self-consistency checking. In Mandayam Srivas and Albert Camilleri, editors, Formal Methods in Computer-Aided Design-FMCAD, volume 1166 of Lecture Notes in Computer Science. Springer-Verlag, 1996."},{"key":"21_CR6","volume-title":"The Java Virtual Machine Specification","author":"T. Lindholm","year":"1996","unstructured":"Tim Lindholm and Frank Yellin. The Java Virtual Machine Specification. Addison Wesley, Reading, Massachusetts, 1996."},{"key":"21_CR7","unstructured":"Steven P. Miller, David A. Greve, Matthew M. Wilding, and Mandayam Srivas. Formal verification of the AAMP-FV microcode. Technical report, Rockwell Collins, Inc., Cedar Rapids, IA, 1996."},{"key":"21_CR8","doi-asserted-by":"crossref","unstructured":"Steven P. Miller and Mandayam Srivas. Formal verification of the AAMP5 microprocessor: A case study in the industrial use of formal methods. In WIFT\u201995: Workshop on Industrial-Strength Formal Specification Techniques, Boca Raton, FL, 1995. IEEE Computer Society.","DOI":"10.1109\/WIFT.1995.515475"},{"key":"21_CR9","volume-title":"The PVS Specification Language (Beta Release)","author":"S. Owre","year":"1993","unstructured":"S. Owre, N. Shankar, and J.M. Rushby. The PVS Specification Language (Beta Release). Computer Science Laboratory, SRI International, Menlo Park, CA, February 1993."},{"key":"21_CR10","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":"21_CR11","volume-title":"The PVS Proof Checker: A Reference Manual (Beta Release)","author":"N. Shankar","year":"1993","unstructured":"N. Shankar, S. Owre, and J. M. Rushby. The PVS Proof Checker: A Reference Manual (Beta Release). Computer Science Laboratory, SRI International, Menlo Park, CA, February 1993."},{"key":"21_CR12","unstructured":"Matthew M. Wilding. Robust computer system proofs in PVS. In C. Michael Holloway and Kelly J. Hayhurst, editors, LFM97: Fourth NASA Langley Formal Methods Workshop. NASA Conference Publication no. 3356, 1997. \n                  http:\/\/atb-www.larc.nasa.gov\/Lfm97\/\n                  \n                ."},{"key":"21_CR13","unstructured":"Alexander Wolfe. First Java-specific MPU rolls. Electronic Engineering Times, page 1, September 22, 1997."}],"container-title":["Lecture Notes in Computer Science","Formal Methods in Computer-Aided Design"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-49519-3_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,24]],"date-time":"2019-02-24T05:31:03Z","timestamp":1550986263000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-49519-3_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540651918","9783540495192"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/3-540-49519-3_21","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1998]]}}}