{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:29:57Z","timestamp":1759638597752},"publisher-location":"Berlin, Heidelberg","reference-count":10,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540556022"},{"type":"electronic","value":"9783540472520"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1992]]},"DOI":"10.1007\/3-540-55602-8_181","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T10:20:16Z","timestamp":1330251616000},"page":"416-430","source":"Crossref","is-referenced-by-count":17,"title":["Automated correctness proofs of machine code programs for a commercial microprocessor"],"prefix":"10.1007","author":[{"given":"Robert S.","family":"Boyer","sequence":"first","affiliation":[]},{"given":"Yuan","family":"Yu","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,8]]},"reference":[{"key":"31_CR1","doi-asserted-by":"crossref","unstructured":"William Bevier, Warren Hunt, J Strother Moore, and William Young. Special issue on system verification. Journal of Automated Reasoning, 5(4), 1989.","DOI":"10.1007\/BF00243131"},{"key":"31_CR2","volume-title":"A Computational Logic","author":"R. S. Boyer","year":"1979","unstructured":"Robert S. Boyer and J. Strother Moore. A Computational Logic. Academic Press, New York, 1979."},{"issue":"1","key":"31_CR3","first-page":"17","volume":"1","author":"R. S. Boyer","year":"1985","unstructured":"Robert S. Boyer and J Strother Moore. Program verification. Journal of Automated Reasoning, 1(1):17\u201323, 1985.","journal-title":"Journal of Automated Reasoning"},{"key":"31_CR4","unstructured":"Robert S. Boyer and J Strother Moore. A Computational Logic Handbook. Academic Press, 1988."},{"key":"31_CR5","unstructured":"Robert S. Boyer and Yuan Yu. A formal specification of some user mode instructions for the Motorola 68020. Technical Report TR-92-04, Computer Sciences Department, University of Texas at Austin, 1992."},{"key":"31_CR6","first-page":"20","volume":"1","author":"J. V. Cook","year":"1990","unstructured":"Jeffrey V. Cook. Verification of the C\/30 microcode using the state delta verification system (SDVS). In 13th National Computer Security Conference, volume 1, pages 20\u201331, 1990.","journal-title":"13th National Computer Security Conference"},{"key":"31_CR7","first-page":"34","volume-title":"John von Neumann, Collected Works, volume V","author":"H. H. Goldstine","year":"1961","unstructured":"Herman H. Goldstine and John von Neumann. Planning and coding problems for an electronic computing instrument. In John von Neumann, Collected Works, volume V, pages 34\u2013235. Pergamon Press, Oxford, 1961."},{"key":"31_CR8","volume-title":"The C Programming Language","author":"B. W. Kernighan","year":"1988","unstructured":"Brian W. Kernighan and Dennis M. Ritchie. The C Programming Language, Second Edition. Prentice Hall, Englewood Cliff, New Jersey, 1988.","edition":"Second Edition"},{"key":"31_CR9","volume-title":"Technical Report CLI-22","author":"J. Strother Moore","year":"1988","unstructured":"J. Strother Moore. Piton: A verified assembly-level language. Technical Report CLI-22, Computational Logic, Inc., Austin, Tx, June 1988."},{"key":"31_CR10","volume-title":"MC68020 32-bit Microprocessor User's Manual","author":"Motorola, Inc.","year":"1989","unstructured":"Motorola, Inc. MC68020 32-bit Microprocessor User's Manual. Prentice Hall, New Jersey, 1989."}],"container-title":["Lecture Notes in Computer Science","Automated Deduction\u2014CADE-11"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-55602-8_181.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:00:16Z","timestamp":1605646816000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-55602-8_181"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1992]]},"ISBN":["9783540556022","9783540472520"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/3-540-55602-8_181","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1992]]}}}