|
| This Article | ||
| | ||
| Share | ||
| Bibliographic References | ||
| Add to: | ||
 Digg  Furl  Spurl  Blink  Simpy  Google  Del.icio.us  Y!MyWeb | ||
| Search | ||
| ||
| ASCII Text | x | ||
| G.B. Leeman, "Some Problems in Certifying Microprograms," IEEE Transactions on Computers, vol. 24, no. 5, pp. 545-553, May, 1975. | |||
| BibTex | x | ||
| @article{ 10.1109/T-C.1975.224258, author = {G.B. Leeman}, title = {Some Problems in Certifying Microprograms}, journal ={IEEE Transactions on Computers}, volume = {24}, number = {5}, issn = {0018-9340}, year = {1975}, pages = {545-553}, doi = {http://doi.ieeecomputersociety.org/10.1109/T-C.1975.224258}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, } | |||
| RefWorks Procite/RefMan/Endnote | x | ||
| TY - JOUR JO - IEEE Transactions on Computers TI - Some Problems in Certifying Microprograms IS - 5 SN - 0018-9340 SP545 EP553 EPD - 545-553 A1 - G.B. Leeman, PY - 1975 KW - Program correctness KW - algebraic simulation KW - abstract program KW - microprogramming KW - commutative diagram KW - theorem proving. VL - 24 JA - IEEE Transactions on Computers ER - | |||
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
Usage of this product signifies your acceptance of the Terms of Use.