|
|
|---|
|
|
|
|---|
Y. Yu, Automated proofs of object code for a widely used
microprocessor
Relevance: details of the operational model of the
Motorola 68020
Abstract
Computing devices can be specified and studied mathematically. Formal specification of computing devices has many advantages — it provides a precise characterization of the computational model and allows for mathematical reasoning about models of the computing devices and programs executed on them. While there has been a large body of research on program proving, work has almost exclusively focused on programs written in high level programming languages. This thesis addresses the very important but largely ignored problem of machine code program proving. In this thesis 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 Proving System. Based on this formal model, we have mechanized a mathematical theory to facilitate automated reasoning about object code programs. We then have mechanically checked the correctness of MC68020 object code programs for binary search, Hoare's Quick Sort, the Berkeley Unix C string library, and other well-known algorithms. The object code for these examples were generated using the Gnu C, the Verdix Ada, and the AKCL common Lisp compilers.
See also the Nqthm scripts