{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T13:31:39Z","timestamp":1754487099956},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540646082"},{"type":"electronic","value":"9783540693390"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0028729","type":"book-chapter","created":{"date-parts":[[2005,12,1]],"date-time":"2005-12-01T06:48:09Z","timestamp":1133419689000},"page":"39-44","source":"Crossref","is-referenced-by-count":9,"title":["Transforming the theorem prover into a digital design tool: From concept car to off-road vehicle"],"prefix":"10.1007","author":[{"given":"David","family":"Hardin","sequence":"first","affiliation":[]},{"given":"Matthew","family":"Wilding","sequence":"additional","affiliation":[]},{"given":"David","family":"Greve","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,18]]},"reference":[{"issue":"4","key":"4_CR1","doi-asserted-by":"crossref","first-page":"411","DOI":"10.1007\/BF00243131","volume":"5","author":"W. R. Bevier","year":"1989","unstructured":"William R. Bevier, Warren A. Hunt Jr., J Strother Moore, and William D. Young.An approach to systems verification. Journal of Automated Reasoning, 5(4):411\u2013428, December 1989.","journal-title":"Journal of Automated Reasoning"},{"key":"4_CR2","doi-asserted-by":"crossref","unstructured":"Mark Bickford and Damir Jamsek. Formal specification and verification of VHDL. 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.","DOI":"10.1007\/BFb0031818"},{"key":"4_CR3","unstructured":"Robert S. Boyer and J Strother Moore. Mechanized formal reasoning about programs and computing machines. In R. Veroff, editor, Automated Reasoning and Its Applications: Essays in Honor of Larry Wos. MIT Press, 1996."},{"issue":"1","key":"4_CR4","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1145\/227595.227603","volume":"43","author":"R. S. Boyer","year":"1996","unstructured":"Robert S. Boyer and Yuan Yu. Automated proofs of object code for a widely used microprocessor. Journal of the ACM, 43(1):166\u2013192, January 1996.","journal-title":"Journal of the ACM"},{"key":"4_CR5","doi-asserted-by":"crossref","unstructured":"Bishop Brock, Matt Kaufmann, and J Strother Moore. ACL2 theorems about commercial microprocessors. 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.","DOI":"10.1007\/BFb0031816"},{"issue":"1","key":"4_CR6","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1023\/A:1008685826293","volume":"11","author":"B. C. Brock","year":"1997","unstructured":"Bishop C. Brock and Jr. Warren A. Hunt. The DUAL-EVAL hardware description language and its use in the formal specification and verification of the FM9001 microprocessor. Formal Methods in System Design, 11(1):71\u2013104, July 1997.","journal-title":"Formal Methods in System Design"},{"key":"4_CR7","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. (submitted for publication)."},{"key":"4_CR8","volume-title":"Symbolic simulation of the JEM1 microprocessor","author":"D. A. Greve","year":"1998","unstructured":"David A. Greve. Symbolic simulation of the JEM1 microprocessor. Technical report, Rockwell Collins, Inc., Cedar Rapids, IA, 1998. (submitted for publication)."},{"key":"4_CR9","unstructured":"David A. Greve and Matthew M. Wilding. Stack-based Java a back-to-future step. Electronic Engineering Times, page 92, January 12, 1998."},{"issue":"4","key":"4_CR10","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1109\/32.588534","volume":"23","author":"M. Kaufmann","year":"1997","unstructured":"M. Kaufmann and J S. Moore. An industrial strength theorem prover for a logic based on Common Lisp. IEEE Transactions on Software Engineering, 23(4):203\u2013213, April 1997.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"4_CR11","volume-title":"Formal verification of the AAMP-FV microcode","author":"S. P. Miller","year":"1996","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":"4_CR12","volume-title":"WIFT'95: Workshop on Industrial-Strength Formal specification Techniques","author":"S. P. Miller","year":"1995","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'95: Workshop on Industrial-Strength Formal specification Techniques, Boca Raton, FL, 1995. IEEE Computer Society."},{"key":"4_CR13","unstructured":"J Strother Moore.Piton-A Mechanically Verified Assembly-Level Language. Kluwer Academic Publishers, 1996."},{"key":"4_CR14","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":"4_CR15","doi-asserted-by":"crossref","unstructured":"David M. Russinoff. A mechanically checked proof of IEEE compliance of the floating point multiplication, division, and square root algorithms of the AMD-K7 processor. Available at www.onr.com\/user\/russ\/david\/, January 28 1998.","DOI":"10.1112\/S1461157000000176"},{"key":"4_CR16","doi-asserted-by":"crossref","unstructured":"Matthew Wilding. A mechanically verified application for a mechanically verified environment. In Costas Courcoubetis, editor, Computer-Aided Verification-CAV '93, volume 697 of Lecture Notes in Computer Science. Springer-Verlag, 1993.","DOI":"10.1007\/3-540-56922-7_22"},{"key":"4_CR17","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, 1997. (http:\/\/atb-www.larc.nasa.gov\/Lfm97\/)."},{"key":"4_CR18","unstructured":"Alexander Wolfe. First Java-specific MPU rolls. Electronic Engineering Times, page 1, September 22, 1997."}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0028729","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,11]],"date-time":"2020-04-11T08:24:04Z","timestamp":1586593444000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0028729"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540646082","9783540693390"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/bfb0028729","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}