Journal of the Association for Computing Machinery, Vol. 43, No. 1, January 1996, pp. 166–192.

Automated Proofs of Object Code for a Widely Used Microprocessor

ROBERT S. BOYER

AND

YUAN YU

Abstract. We have formally described a substantial subset of the MC68020, a widely used microprocessor built by Motorola, within the mathematical logic of the automated reasoning system Nqthm, a.k.a. the Boyer-Moore Theorem Prover. Using this formal description, we have mechanically checked the correctness of MC68020 object code programs for binary search, Hoare’s Quick Sort, twenty-one functions from the Berkeley Unix C string library, and other well-known algorithms. The object code for these examples was generated using the Gnu C, the Verdix Ada, and the Gnu Common Lisp compilers. We have mechanized a mathematical theory to facilitate automated reasoning about object code programs. We describe a two-stage methodology we use to do our proofs.

Categories and Subject Descriptors. D.2.1 [Software Engineering]: Requirements/ Specifications; D.2.4 [Software Engineering]: Program Verification; D.3.1 [Programming Languages]: Formal Definitions and Theory; F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs; I.2.3 [Artificial Intelligence]: Deduction and Theorem Proving

General Terms. Theory

Additional Key words and Phrases. Ada, automated reasoning, Boyer-Moore logic, C, Common Lisp, formal methods, machine code, mechanical theorem proving, MC68xxx, Nqthm, object code, program proving, program verification

Copyright 1996 by ACM, Inc. Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or direct commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, to republish, to post on servers, or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from Publications Dept, ACM Inc., fax +1 (212) 869-0481, or permissions@acm.org.