An approach to systems verification
Tóm tắt
Từ khóa
Tài liệu tham khảo
Bevier, W. R., ‘Kit and the short stack’ (in this issue of The Journal of Automated Reasoning).
Bevier, W. R., ‘Kit: A study in operating system verification’ (to appear in IEEE Trans. on Soft. Eng.). Also available as Tech. Rept 28, Computational Logic, Inc., 1717 West Sixth Street, Suite 290, Austin, Texas, 78703.
Boyer, R. S. and Moore, J S., ‘Metafunctions: Proving them correct and using them efficiently as new proof procedures’, In The Correctness Problem in Computer Science (eds R. S. Boyer and J S. Moore), Academic Press, London, 1981.
Boyer, R. S. and Moore, J S., ‘A fast string searching algorithm’, Comm. ACM 20, 10 (1977), 762–772.
Boyer, R. S. and Moore, J S., ‘A verification condition generator for FORTRAN’, In The Correctness Problem in Computer Science (eds R. S. Boyer and J S. Moore), Academic Press, London, 1981.
Boyer, R. S. and Moore, J S., ‘MJRTY — a fast majority vote algorithm’, Tech. Rept ICSCA-CMP-32, Institute for Computing Science and Computer Applications, Univ. of Texas at Austin, 1982. Also available through Computational Logic, Inc., Suite 290, 1717 West Sixth Street, Austin, TX 78703.
Boyer, R. S. and Moore, J S., ‘Proof checking the RSA public key encryption algorithm’, Amer. Math. Monthly 91, 3 (1984), 181–189.
Boyer, R. S. and Moore, J. S., A Computational Logic Handbook, Academic Press, Boston, 1988.
Good, D. I., Cohen, R. M., and Keeton-Williams, J., ‘Principles of proving concurrent programs in Gypsy’, Tech. Rept ICSCA-CMP-15, Institute for Computer Science and Computing Applications, Univ. of Texas at Austin, January, 1979.
Hunt, W. A., ‘Microprocessor design verification’ (in this issue of The Journal of Automated Reasoning).
Kaufmann, Matt, A user's manual for an interactive enhancement to the Boyer-Moore theorem prover’, Tech. Rept CLI-19, CLInc, May, 1988.
Lengauer, C. and Huang, C.-H., ‘A mechanically certified theorem about optimal concurrency of sorting networks’, Proc. 13th Ann. ACM Symp. on Principles of Programming Languages, 1986, pp. 307–317.
Moore, J S., A mechanically verified language implementation’ (in this issue of The Journal of Automated Reasoning). Also available as Tech. Rept 30, Computational Logic, Inc., 1717 West Sixth Street, Suite 290, Austin, Texas, 78703.
Shankar, N., ‘Proof checking metamathematics’, Univ. of Texas at Austin, 1986. Also available through Computational Logic, Inc., Suite 290, 1717 West Sixth Street, Austin, TX 78703.
Young, W. D., ‘A mechanically verified code generator’ (in this issue of The Journal of Automated Reasoning). Also available as Tech Rept 36, Computational Logic, Inc., 1717 West Sixth Street, Suite 290, Austin, Texas, 78703.