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.

Lattice operations such as greatest lower bound (GLB), least upper bound (LUB), and relative complementation (BUTNOT) are becoming more and more important in programming languages supporting object inheritance. We present a general technique for the efficient implementation of such operations based on an encoding method. The effect of the encoding is to plunge the given ordering into a boolean lattice of binary words, leading to an almost constant time complexity of the lattice operations. A first method is described based on a transitive closure approach. Then a more space-efficient method minimizing code-word length is described. Finally a powerful grouping technique called modulation is presented, which drastically reduces code space while keeping all three lattice operations highly efficient. This technique takes into account idiosyncrasies of the topology of the poset being encoded that are quite likely to occur in practice. All methods are formally justified. We see this work as an original contribution towards using semantic (vz., in this case, taxonomic) information in the engineering pragmatics of storage and retrieval of (vz., partially or quasi-ordered) information.

A proof by a computer program of the unsolvability of the halting problem is described.The halting problem is posed in a construcUve, formal language.The computational paradigm formalized ~s Pure LISP, not Tunng machines.The machine was led to the proof by the authors, who suggested certain function definitions and stated certain intermediate lemmas.The machine checked to ascertain that every suggested definition was admissible and the machine proved the main theorem and every lemma.It is beheved this is the first instance of a machine checking that a given problem is not solvable by machine.

We describe how to transform certain flowchart programs into equivalent explicit primitive recursive programs. The input/output correctness conditions for the transformed programs are more amenable to proof than the verification conditions for the corresponding flowchart programs. In particular, the transformed correctness conditions can often be verified automatically by the theorem prover developed by Boyer and Moore [1].

Program verification is the 1den that propertms of programs can be precisely stated and proved in the mathematical sense.In th~s paper, some simple heuristics combimng evaluation and mathematical reduction are described, which the authors have implemented in a program that automatlcally proves a wide varietyof theorems about recursive Lisp functions.The method the program uses to generate induction formulas is described at length The theorems proved by the program include that REVERSE is its own inverse and that a particular SORT program is correct.A list of theorems proved by the program is given KEY WORDS AND PHRASES.