AUTOMATED PROOFS OF OBJECT CODE FOR A WIDELY USED MICROPROCESSOR

We have formally described a substantial subset of the MC68020, a wide ly used microprocessor built by Motorola, within the mathematical logi c of the automated reasoning system Nqthm, a.k.a. the Boyer-Moore Theo rem Prover [Boyer and Moore 1988]. Using this formal description, we h ave mechanically checked the correctness of MC68020 object code progra ms for binary search, Hoare's Quick Sort, twenty-one functions from th e Berkeley Unix C string library, and other well-known algorithms. The object code for these examples was generated using the Gnu C, the Ver dix Ada, and the Gnu Common Lisp compilers. We have mechanized a mathe matical theory to facilitate automated reasoning about object code pro grams. We describe a two-stage methodology we use to do our proofs.