The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.05 - May (1975 vol.24)
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. 5, pp. 545-553, May 1975, doi:10.1109/T-C.1975.224258
15 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool