Issue No. 05 - May (1975 vol. 24)
G.B. Leeman , Department of Computer Science, IBM Thomas J. Watson Research Center
A hypothetical computer is described, and procedures are indicated for showing the correctness of its microprogram. The underlying method used is that of Birman . However, the computer discussed has some realistic characteristics not shared by the machine treated in , and the details of the microcode validation are complicated by this fact. A formal technique for partitioning the proof is presented and illustrated with examples.
Program correctness, algebraic simulation, abstract program, microprogramming, commutative diagram, theorem proving.
G. Leeman, "Some Problems in Certifying Microprograms," in IEEE Transactions on Computers, vol. 24, no. , pp. 545-553, 1975.