The Community for Technology Leaders
Green Image
Issue No. 05 - May (1975 vol. 24)
ISSN: 0018-9340
pp: 545-553
G.B. Leeman , Department of Computer Science, IBM Thomas J. Watson Research Center
ABSTRACT
A hypothetical computer is described, and procedures are indicated for showing the correctness of its microprogram. The underlying method used is that of Birman [1]. However, the computer discussed has some realistic characteristics not shared by the machine treated in [1], 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.
INDEX TERMS
Program correctness, algebraic simulation, abstract program, microprogramming, commutative diagram, theorem proving.
CITATION
G.B. Leeman, "Some Problems in Certifying Microprograms", IEEE Transactions on Computers, vol. 24, no. , pp. 545-553, May 1975, doi:10.1109/T-C.1975.224258
94 ms
(Ver )