|
|
|---|
|
|
|
|---|
R. S. Boyer and Y. Yu, “Automated Proofs of
Object Code for a Widely Used Microprocessor”, Journal of the
ACM 43(1), pp. 166-192, January, 1996.
Relevance: operational model of the Motorola 68020
and verification of object code generated by commercial compilers
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 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 AKCL 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.
See also the Nqthm scripts