{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,14]],"date-time":"2026-02-14T09:02:48Z","timestamp":1771059768523,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":38,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540619376","type":"print"},{"value":"9783540495673","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/bfb0031816","type":"book-chapter","created":{"date-parts":[[2005,12,11]],"date-time":"2005-12-11T06:59:01Z","timestamp":1134284341000},"page":"275-293","source":"Crossref","is-referenced-by-count":59,"title":["ACL2 theorems about commercial microprocessors"],"prefix":"10.1007","author":[{"given":"Bishop","family":"Brock","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Matt","family":"Kaufmann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J Strother","family":"Moore","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,25]]},"reference":[{"key":"21_CR1","volume-title":"CAP Technical Report 9","author":"K. Albin","year":"1995","unstructured":"K. Albin. Validating the ACL2 CAP Model. CAP Technical Report 9, Computational Logic, Inc., 1717 W. 6th, Austin, TX 78703 March, 1995."},{"key":"21_CR2","volume-title":"A Computational Logic","author":"R. S. Boyer","year":"1979","unstructured":"R. S. Boyer and J. S. Moore. A Computational Logic. Academic Press: NewYork, 1979."},{"key":"21_CR3","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: New York, 1988."},{"issue":"1","key":"21_CR4","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. Automated Proofs of Object Code for a Widely Used Microprocessor, JACM, 43(1) January, 1996, pp. 166\u2013192.","journal-title":"JACM"},{"key":"21_CR5","volume-title":"CAP Technical Report 8","author":"B. Brock","year":"1995","unstructured":"B. Brock. The CAP 94 Specification, CAP Technical Report 8, Computational Logic, Inc., 1717 W. 6th, Austin, TX 78703, July, 1995."},{"key":"21_CR6","volume-title":"CAP Technical Report 10","author":"B. Brock","year":"1996","unstructured":"B. Brock. Formal Analysis of the CAP Instruction Pipeline, CAP Technical Report 10, Computational Logic, Inc., 1717 W. 6th, Austin, TX 78703, June, 1996."},{"key":"21_CR7","volume-title":"CAP Technical Report 15","author":"B. Brock","year":"1996","unstructured":"B. Brock. Formal Verification of CAP Applications, CAP Technical Report 15, Computational Logic, Inc., 1717 W. 6th, Austin, TX 78703, June, 1996."},{"key":"21_CR8","unstructured":"R. E. Bryant. Bit-Level Analysis of an SRT Divider Circuit, CMU-CS-95-140, School of Computer Science, Carnegie Mellon University, Pittsburg, PA 15213."},{"key":"21_CR9","doi-asserted-by":"crossref","unstructured":"R. E. Bryant and Y. A. Chen. Verification of arithmetic functions with binary moment diagrams. In Proceedings of the 32nd ACM\/IEEE Design Automation Conference IEEE Computer Society Press, June 1995.","DOI":"10.1145\/217474.217583"},{"issue":"4","key":"21_CR10","doi-asserted-by":"crossref","first-page":"401","DOI":"10.1109\/43.275352","volume":"13","author":"J. R. Burch","year":"1994","unstructured":"J. R. Burch, E. M. Clarke, D. E. Long, K. L. McMillan and D. L. Dill. Symbolic Model Checking for Sequential Circuit Verification, IEEE Trans. on Computer-Aided Design of Integrated Circuits and Systems 13(4) April, 1994, pp. 401\u2013424.","journal-title":"IEEE Trans. on Computer-Aided Design of Integrated Circuits and Systems"},{"key":"21_CR11","first-page":"68","volume-title":"Lecture Notes in Computer Science Volume 818","author":"J. R. Burch","year":"1994","unstructured":"J. R. Burch and D. L. Dill. Automatic verification of pipelined microprocessor control. in David Dill, editor, Computer-Aided Verification, CAV '94, Stanford, CA, Springer-Verlag, Lecture Notes in Computer Science Volume 818, June, 1994, pp. 68\u201380."},{"key":"21_CR12","doi-asserted-by":"crossref","unstructured":"E. M. Clarke, S. M. German and X. Zhao. Verifying the SRT Division Algorithm using Theorem Proving Techniques, Proceedings of Conference on Computer-Aided Verification, CAV '96, July, 1996.","DOI":"10.1007\/3-540-61474-5_62"},{"key":"21_CR13","unstructured":"E. M. Clarke, M. Fujita, and X. Zhao. Hybrid Decision Diagrams, ICCAD95, 1995, pp. 159\u2013163."},{"key":"21_CR14","unstructured":"E. M. Clarke, O. Grumberg, H. Hiraishi, S. Jha, D. E. Long, K. L. McMillan and L. A. Ness. Verification of the Futurebus+ Cache Coherence Protocol, Proc. CHDL, 1993."},{"key":"21_CR15","unstructured":"J. Crow, S. Owre, J. Rushby, N. Shankar, and M. Srivas. A Tutorial Introduction to PVS, presented at Workshop on Industrial-Strength Formal Specification Techniques, Boca Raton, FL, April 1995 (see http:\/\/www.csl.sri.com\/pvs.html)."},{"key":"21_CR16","doi-asserted-by":"crossref","unstructured":"S. Gilfeather, J. Gehman, and C. Harrison. Architecture of a Complex Arithmetic Processor for Communication Signal Processsing in SPIE Proceedings, International Symposium on Optics, Imaging, and Instrumentation, 2296 Advanced Signal Processing: Algorithms, Architectures, and Implementations V, July, 1994, pp. 624\u2013625.","DOI":"10.1117\/12.190874"},{"issue":"1","key":"21_CR17","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1002\/j.1538-7305.1990.tb00102.x","volume":"69","author":"Z. Har'El","year":"1990","unstructured":"Z. Har'El and R. P. Kurshan. Software for Analytical Development of Communications Protocols, AT&T Bell Laboratories Technical Journal, 69(1) Jan\u2013Feb, 1990, pp. 45\u201359.","journal-title":"AT&T Bell Laboratories Technical Journal"},{"key":"21_CR18","volume-title":"CAP Technical Report 16","author":"C. Harrison","year":"1995","unstructured":"C. Harrison. Hardware Verification of the Complex Arithmetic Processor XY Address Generator. CAP Technical Report 16, Computational Logic, Inc., 1717 W. 6th, Austin, TX 78703, August, 1995."},{"issue":"4","key":"21_CR19","doi-asserted-by":"crossref","first-page":"429","DOI":"10.1007\/BF00243132","volume":"5","author":"W. A. Hunt Jr.","year":"1989","unstructured":"W. A. Hunt, Jr. Microprocessor Design Verification. Journal of Automated Reasoning, 5(4), pp. 429\u2013460, 1989.","journal-title":"Journal of Automated Reasoning"},{"key":"21_CR20","unstructured":"W. A. Hunt, Jr. and B. Brock. A Formal HDL and its use in the FM9001 Verification. Proceedings of the Royal Society, 1992."},{"key":"21_CR21","volume-title":"CAP Technical Report 12","author":"W. A. Hunt Jr.","year":"1996","unstructured":"W. A. Hunt, Jr. CAP Pin-level Specifications, CAP Technical Report 12, Computational Logic, Inc., 1717 W. 6th, Austin, TX 78703, April, 1996."},{"key":"21_CR22","unstructured":"M. Kaufmann and J S. Moore. High-Level Correctness of ACL2: A Story, URL ftp:\/\/ftp.cli.com\/pub\/acl2\/v1-8\/acl2-sources\/reports\/story.txt, September, 1995."},{"key":"21_CR23","unstructured":"M. Kaufmann and J S. Moore. ACL2 Version 1.8, URL ftp:\/\/ftp.cli.-com\/pub\/acl2\/v1-8\/acl2-sources\/doc\/HTML\/acl2-doc.html, 1995."},{"key":"21_CR24","doi-asserted-by":"crossref","unstructured":"M. Kaufmann and J S. Moore. ACL2: An Industrial Strength Version of Nqthm. In Proceedings of the Eleventh Annual Conference on Computer Assurance (COMPASS-96), IEEE Computer Society Press, June, 1996, pp. 23\u201334.","DOI":"10.1109\/CMPASS.1996.507872"},{"issue":"1\u20132","key":"21_CR25","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1007\/BF00244463","volume":"16","author":"M. Kaufmann","year":"1996","unstructured":"M. Kaufmann and P. Pecchiari. Interaction with the Boyer-Moore and Theorem Prover: A Tutorial Study Using the Arithmetic-Geometric Mean Theorem. Journal of Automated Reasoning 16(1\u20132) March, 1996, pp. 181\u2013222.","journal-title":"Journal of Automated Reasoning"},{"key":"21_CR26","doi-asserted-by":"crossref","unstructured":"S. P. Miller and M. Srivas. Formal Verification of the AAMP5 Microprocessor: A Case Study in the Industrial Use of Formal Methods, in Proceedings of WIFT '95: Workshop on Industrial-Strength Formal Specification Techniques, IEEECS, April, 1995, pp. 2\u201316.","DOI":"10.1109\/WIFT.1995.515475"},{"key":"21_CR27","volume-title":"NASA Technical Memorandum 110167","author":"P. M. Miner","year":"1995","unstructured":"P. M. Miner. Defining the IEEE-854 Floating-Point Standard in PVS, NASA Technical Memorandum 110167, NASA Langely Research Center, Hampton, VA 23681, 1995."},{"key":"21_CR28","unstructured":"J S. Moore. Piton: A Mechanically Verified Assembly-Level Language, Automated Reasoning Series, Kluwer Academic Publishers, 1996."},{"key":"21_CR29","unstructured":"J S. Moore, T. Lynch, and M. Kaufmann. A Mechanically Checked Proof of the Correctness of the Kernel of the AMD5K86 Floating-Point Division Algorithm, March, 1996, URL http:\/\/devil.ece.utexas.edu:80\/\u223clynch\/divide\/-divide.html."},{"key":"21_CR30","volume-title":"Discrete-Time Signal Processing","author":"A. V. Oppenheim","year":"1989","unstructured":"A. V. Oppenheim and R. W. Scahfer. Discrete-Time Signal Processing. Prentice Hall, Englewood Cliffs, New Jersey, 1989."},{"key":"21_CR31","unstructured":"K. M. Pitman et al. drafi proposed American National Standard for Information Systems \u2014 Programming Language \u2014 Common Lisp; X3J13\/93-102.Global Engineering Documents, Inc., 1994."},{"key":"21_CR32","volume-title":"Modular Verification of SRT Division","author":"H. Ruess","year":"1996","unstructured":"H. Ruess, M. K. Srivas, and N. Shankar. Modular Verification of SRT Division, Computer Science Laboratory, SRI International, Menlo Park, CA 49025, 1996."},{"key":"21_CR33","doi-asserted-by":"crossref","unstructured":"M. Srivas and M. Bickford. Formal Verification of a Pipelined Microprocessor, IEEE Software, September, 1990, pp. 52\u201364.","DOI":"10.1109\/52.57892"},{"issue":"3","key":"21_CR34","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1007\/BF01384049","volume":"4","author":"V. Stavridou","year":"1994","unstructured":"V. Stavridou. Gordon's Computer: A Hardware Verification Case Study in OBJ3, Formal Methods in System Design, 4(3), 1994, pp. 265\u2013310.","journal-title":"Formal Methods in System Design"},{"key":"21_CR35","volume-title":"Common LISP: The Language","author":"G. L. Steele Jr.","year":"1984","unstructured":"G. L. Steele, Jr. Common LISP: The Language, Digital Press: Bedford, MA, 1984."},{"key":"21_CR36","volume-title":"Common Lisp The Language","author":"G. L. Steele Jr.","year":"1990","unstructured":"G. L. Steele, Jr. Common Lisp The Language, Second Edition. Digital Press, 30 North Avenue, Burlington, MA 01803, 1990.","edition":"Second Edition"},{"key":"21_CR37","doi-asserted-by":"crossref","unstructured":"U. Stern and D. L. Dill. Automatic Verification of the SCI Cache Coherence Protocol, in Proceedings of IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, 1995, pp. 21\u201334.","DOI":"10.1007\/3-540-60385-9_2"},{"key":"21_CR38","volume-title":"Technical Report 92","author":"Y. Yu","year":"1993","unstructured":"Y. Yu. Automated Proofs of Object Code for a Widely used Microprocessor, Technical Report 92, Computational Logic, Inc., 1717 W. 6th, Austin, TX 78703, May, 1993. URL http:\/\/www.cli.com\/reports\/files\/92.ps."}],"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\/BFb0031816","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,6]],"date-time":"2025-01-06T12:11:40Z","timestamp":1736165500000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0031816"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540619376","9783540495673"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/bfb0031816","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1996]]}}}