Robert S. Boyer
- BEVIER, W. 1987. A verified operating system kernel. Ph.D. dissertation. Univ. Texas at Austin, Austin, Tex. Google Scholar
- BEVIER, W., HUNT, W., MOORE, j. S., AND YOUNG, W. 1989. Special issue on system verification. J. Aurora. Reas. 5, 4, 409-530. Google Scholar
- BOYER, R. S., AND MOORE, J. S. 1981. Metafunctions: Proving them correct and using them efficiently as new proof procedures. In The Correctness Problem in Computer Science, R. S. Boyer and J. S. Moore, eds. Academic Press, London, pp. 103-184.Google Scholar
- BOYER, R. S., AND MOORE, J. S. 1985. Program verification. J. Autom. Reas. 1, 1, 17-23. Google Scholar
- BORER, R. S., AND MOORE, J. S. 1979. A Computational Logic. Academic Press, New York.Google Scholar
- BOYER, R. S., ,~'~D MOORE, J. S. 1988. A Computational Logic Handbook. Academic Press, New Google Scholar
- York. For sources and examples, see ftp://ftp.cli.com/pub/nqthm/nqthm-1992/nqthm- 1992.tar.Z or ftp://ftp.cs.utexas.edu/pub/boyer/nqthm- 1992.tar.Z.Google Scholar
- BO~R, R. S., AND YU. Y. 1992. A formal specification of some user mode instructions for the Motorola 68020. Technical Report TR-92-04, Computer Sciences Department, University of Texas at Austin, 1992. See ftp://ftp.cs.utexas.edu/pub/techreports/tr92-O4.ps.Z. Alternatively, see examples/yu/mc20-1 .ps in ftp: //ftp.cs.utexas.edu/pub/boyer/nqthm- 1992.tar.Z. Google Scholar
- CLtrr~UCK, D. L., AND CARRf~, B. A. 1988. The verification of low-level code. IEE Softw. Eng. J., 97-111. Google Scholar
- CORN, A. 1987. A proof of correctness of the Viper microprocessor: The first level. Tech. Rep. 104. Univ. Cambridge, Cambridge, England.Google Scholar
- CooK, J. V. 1990. Verification of the C/30 microcode using the State Delta Verification System (SDVS). In Proceedings of the 13th National Computer Security Conference. Vol. 1. National Institute of Standards/National Computer Security Center, Maryland pp. 20-31.Google Scholar
- FLOYD, R. W. 1967. Assigning meanings to programs. In Mathematical Aspects of Computer Science, tS'oceedings of Symposia in Applied Mathematics. American Mathematical Society, Providence, R.I., pp. 19-32.Google Scholar
- GOLDSTINE, H. H., AND VON NEUMANN, J. 1961. Planning and coding problems for an electronic computing instrument. In John yon Neumann, Collected Works, Vol. V. Pergamon Press, Oxford, England, pp. 34-235.Google Scholar
- HOARE, C. A. R. 1969. An axiomatic basis for computer programming. Commun. ACM 12, 10 (Oct.). 576-583. Google Scholar
- HUNT, W. A. 1985. FM8501: A verified microprocessor. Ph.D. dissertation, Univ. Texas at Austin, Austin, Tex. Google Scholar
- O'NEILL, I. M., CLUTI~RBUCK, D. L., FARROW, P. F., SUMMERS, P. G., AUO DOLMAN, W. C. 1988. The formal verification of safety-critical assembly code. In Safety of Computer Control System 1988. Pergamon Press, Oxford, England.Google Scholar
- ISO COMMITTEE JTCI/SC22/WG14. 1990. ISO/IEC 9899:1990. International Standards Organization, Geneva, (Available from the American National Standards Institute, 11 West 42nd Street, New York, NY 10236).Google Scholar
- KERr~tGHAN, B. W., AND RITCHIE, D. M. 1988. The C Programming Language, 2nd ed. Prentice- Hail, Englewood Cliffs, N.J. Google Scholar
- KNUTH, D. E. 1981. The Art of Computer Programming, Vol. 1. Addison-Wesley, Reading, Mass. Google Scholar
- MAURER, W. D. 1974. Some correctness principles for machine language program and microprocessors. In Proceedings of the 7th Annual Workshop on Microp~mming, (Palo Alto, Calif.). Google Scholar
- I~AURER, W. D. 1977. An IBM 370 assembly language verifier. In Proceedings of the 16th Annual Technical Symposium on Systems and Software: Operational Reliability and Performance Assurance. ACM, New York, pp. 139-146.Google Scholar
- MCCARTHY, J. 1962. Towards a mathematical science of computation. In Proceedings of IFIP Congress. pp. 21-28.Google Scholar
- MOORE, J. S. 1996. th'ton: A Mechanically Verified Assembly--Level Language. Kluwer, Dordrecht, to appear. Google Scholar
- MOTOROLA, INC. 1989. MC68020 32-bit Microprocessor User's Manual. Prentice-Hall, Englewood Cliffs, N.J. Google Scholar
- PLAUGER, P. J. 1992. The Standard C Library. Prentice-Hall, Englewood Cliffs, N.J. Google Scholar
- POLAK, W. 1981. Compiler Specification and Verification. Springer-Verlag, Berlin, Germany. Google Scholar
- SITES, R. L. 1992. Alpha Architecture Reference Manual. Digital Press, Bedford, Mass. Google Scholar
- TUmNG, A. M. 1949. On checking a large routine, in Report of a Conference on High Speed Automatic Calculating Machines. Univ. Math. Laboratory, Cambridge, England, pp. 67-69. ANSI COMMITTEE X3Jll. ANSI X3.159-1989. American National Standards Institute, New York.Google Scholar
- Yu, Y. 1992. Automated Proofs of Object Code for a W'utety Used Microprocessor. Ph.D. dissertation, University of Texas at Austin, Austin, Tex. For the dissertation text, see ftp://ftp.cs.utexas.edu/pub/techreports/tr93-09.ps.Z. See the files ./examples/yu/* in ftp://ftp.cs.utexas.edu/pub/boyer/nqthm-1992.tar.Z for replayable proof scripts of all the definitions and theorems mentioned in this paper and in the thesis. Google Scholar
Index Terms
- Automated proofs of object code for a widely used microprocessor
Recommendations
The Reflective Milawa Theorem Prover is Sound (Down to the Machine Code that Runs it)
This paper presents, we believe, the most comprehensive evidence of a theorem prover's soundness to date. Our subject is the Milawa theorem prover. We present evidence of its soundness down to the machine code. Milawa is a theorem prover styled after ...
Reviews
Richard John Botting
Boyer and Yu have combined the disciplines of formal hardware specification, automatic theorem proving, and program proving. They show that real libraries and subroutines can be proven correct at the hardware level. They have verified code for an MC68020 processor compiled from C and Ada subprograms. A growing library of lemmas guided the automatic theorem prover. Verifying machine code is not a new idea. Twenty-five years ago a peripheral arrived a month after I had finished its driver. I had time to prove the code by hand. We saved time later because I knew, for once, that the bugs were not in my code. This paper is a readable summary of doctoral work. It answers some criticisms of mathematical and logical methods. Anyone who develops software that must work as specified should read it.
Access critical reviews of Computing literature here
Become a reviewer for Computing Reviews.
Comments