George B. Leeman
Duke Mathematical Journal
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. Copyright © 1975 by The Institute of Electrical and Electronics Engineers, Inc.
George B. Leeman
Duke Mathematical Journal
George B. Leeman
Trans. Am. Math. Soc.
George B. Leeman
Pacific Journal of Mathematics
George B. Leeman
Proceedings of the American Mathematical Society