Automated proofs of object code for a widely used microprocessor
Robert S. Boyer, Yuan Yu · Journal of the ACM · 1996
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 19881.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.