AbstractWe 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 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.
The abstract is also available as a LaTeX file, a DVI file, or a PostScript file.
Categories and Subject Descriptors: D.2.1 [Software Engineering]: Requirements/Specifications; D.2.4 [Software Engineering]: Program Verification; D.3.1 [Programming Languages]: Formal Definitions and Theory; F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs; I.2.3 [Artificial Intelligence]: Deduction and Theorem Proving
General Terms: Theory
Additional Key Words and Phrases: Ada, automated reasoning, Boyer-Moore logic, C, Common Lisp, formal methods, machine code, mechanical theorem proving, MC68xxx, Nqthm, object code, program proving, program verification
Selected papers that cite this one
- George C. Necula. Proof-carrying code. In Conference Record of POPL '97: The 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 106-119, Paris, France, 15-17 January 1997.
Selected references
- C. A. R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10):576-580, 583, October 1969.