{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T13:37:29Z","timestamp":1754487449800,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":5,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540665595"},{"type":"electronic","value":"9783540481539"}],"license":[{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48153-2_23","type":"book-chapter","created":{"date-parts":[[2010,3,29]],"date-time":"2010-03-29T21:13:28Z","timestamp":1269897208000},"page":"313-316","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Results of the Verification of a Complex Pipelined Machine Model"],"prefix":"10.1007","author":[{"given":"Jun","family":"Sawada","sequence":"first","affiliation":[]},{"suffix":"Jr.","given":"Warren A.","family":"Hunt","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,6,3]]},"reference":[{"key":"23_CR1","doi-asserted-by":"crossref","unstructured":"Matt Kaufmann and J Strother Moore. ACL2: An industrial strength version of nqthm. In Eleventh Annual Conference on Computer Assurance (COMPASS-96), pages 23\u201334. IEEE computer Society Press, June 1996.","DOI":"10.1109\/CMPASS.1996.507872"},{"key":"23_CR2","first-page":"1159","volume-title":"Handbook of Theoretical Computer Science","author":"L. Lamport","year":"1990","unstructured":"Leslie Lamport and Nancy Lynch. Distributed computing models and methods. In Handbook of Theoretical Computer Science, volume B, pages 1159\u20131199. The MIT Press, Cambridge, Ma., 1990."},{"key":"23_CR3","unstructured":"Jun Sawada. Verification scripts for FM9801 pipelined microprocessor design. Web page http:\/\/www.cs.utexas.edu\/users\/sawada\/FM9801\/ ."},{"key":"23_CR4","unstructured":"Jun Sawada and Warren A. Hunt, Jr. Verification of FM9801: Out-of-order processor with speculative execution and exceptions that may execute self modifying code. Unpublished Report. Personal contact: sawada@cs.utexas.edu."},{"key":"23_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/BFb0028740","volume-title":"computer Aided Verification (CAV\u2019 98)","author":"J. Sawada","year":"1998","unstructured":"Jun Sawada and Warren A. Hunt, Jr. Processor verification with precise exceptions and speculative execution. In Alan J. Hu and Moshe Y. Vardi, editors, computer Aided Verification (CAV\u2019 98), volume 1427 of LNCS, pages 135\u2013146. Springer Verlag, 1998."}],"container-title":["Lecture Notes in Computer Science","Correct Hardware Design and Verification Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48153-2_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,19]],"date-time":"2025-02-19T19:16:18Z","timestamp":1739992578000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48153-2_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540665595","9783540481539"],"references-count":5,"URL":"https:\/\/doi.org\/10.1007\/3-540-48153-2_23","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]},"assertion":[{"value":"3 June 2003","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}