Automated proofs of object code for a widely used microprocessor

1 January 1996

journal article
research article
Published by Association for Computing Machinery (ACM) in Journal of the ACM

Vol. 43 (1) , 166-192
https://doi.org/10.1145/227595.227603

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 [Boyer and Moore 1988]. 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.

Keywords

This publication has 4 references indexed in Scilit:

The verification of low-level code
Software Engineering Journal, 1988
Compiler Specification and Verification
Published by Springer Nature ,1981
An axiomatic basis for computer programming
Communications of the ACM, 1969
Assigning meanings to programs
Published by American Mathematical Society (AMS) ,1967