Automated Correctness Proofs of Machine Code Programs for a Commercial Microprocessor

. We have formally specified a substantial subset of the MC68020, a widely used microprocessor built by Motorola, within the mathematical logic of the automated reasoning system Nqthm, i.e., the Boyer-Moore Theorem Prover [6]. Using this MC68020 specification, we have mechanically checked the correctness of MC68020 machine code programs for Euclid's GCD, Hoare's Quick Sort, binary search, and other well-known algorithms. The machine code for these examples was generated using the Gnu C and the Verdix Ada compilers. We have developed an extensive library of proven lemmas to facilitate automated reasoning about machine code programs. We describe a two stage methodology we use to do our machine code proofs. Key words. Automated reasoning, Nqthm, Boyer-Moore Theorem Prover, formal program verification, object code, Gnu, C, Ada. 1 Introduction One of the main reasons for our lack of confidence in computing systems is the lack of mathematical theories to forecast accurately the behavior of ..