Advertisement

Springer Nature is making Coronavirus research free. View research | View latest news | Sign up for updates

A mechanically verified code generator

  • 53 Accesses

  • 33 Citations

Abstract

We describe the specification, implementation and proof of correctness of a code generator for a subset of Gypsy 2.05. The code generator is specified in the Boyer-Moore logic; its proof is fully machine-checked using the Kaufmann-enhanced Boyer-Moore theorem prover. Our code generator sits atop a ‘stack’ of verified system components providing a prototype development environment for constructing highly reliable application Programs.

This is a preview of subscription content, log in to check access.

References

  1. 1.

    Aubin, R., ‘Mechanizing structural induction’, PhD Thesis, Univ. of Edinburgh, Edinburgh, Scotland, 1976.

  2. 2.

    Bevier, W. R., ‘Kit: A study in operating system verification’, Tech. Rept CLI-28, Computational Logic, Inc., August, 1988.

  3. 3.

    Bevier, W. R., Hunt, W. A., Moore, J S., and Young, W. D., ‘An approach to system verification’ (in this issue of The Journal of Automated Reasoning).

  4. 4.

    Boyer, R. S. and Moore, J S., A Computational Logic, Academic Press, New York, 1979.

  5. 5.

    Boyer, R. S. and Moore, J S., A Computational Logic Handbook, Academic Press, New York, 1988.

  6. 6.

    Burstall, R. M., ‘Proving properties of programs by structural induction’, Computer J. 12, 1 (February, 1969), 41–48.

  7. 7.

    Cartwright, R., ‘A practical formal semantic definition and verification system for typed LISP’, PhD Thesis, Stanford Univ., 1976.

  8. 8.

    Chirica, L. M. and Martin, D. F., ‘An approach to compiler correctness’, Proceedings of the International Conference on Reliable Software, April, 1975, pp. 96–103.

  9. 9.

    Cohn, A., ‘Machine assisted proofs of recursion implementation’, PhD Thesis, Univ. of Edinburgh, Edinburgh, Scotland, 1979.

  10. 10.

    Good, D. I., Akers, R. L. and Smith, L. M., ‘Report on Gypsy 2.05’, Tech. Rept CLI-1, Computational Logic, Inc., October, 1986.

  11. 11.

    Good, D. I., Divito, B. L. and Smith, M. K., ‘Using the Gypsy methodology’, Tech. Rept Draft CLI-2, Computational Logic, Inc., January, 1988.

  12. 12.

    Henhapl, W. and Jones, C. B., ‘The block structure concept and some possible implementations’, Tech. Rept 25.104, IBM Laboratories, Vienna, 1970.

  13. 13.

    Hunt, W. A., ‘The mechanical verification of a microprocessor design’, Tech. Rept CLI-6, Computational Logic, Inc., September, 1986.

  14. 14.

    Kaufmann, Matt, ‘A user's manual for an interactive enhancement to the Boyer-Moore theorem prover’, Tech. Rept CLI-19, Computational Logic, Inc., May, 1988.

  15. 15.

    Lucas, P., ‘Two constructive realizations of the block concept and their realization’, Tech. Rept 25.082, IBM Laboratories, Vienna, 1968.

  16. 16.

    Lynn, D. S., ‘Interactive compiler proving using Hoare proof rules’, Tech. Rept ISI/RR-78-70, Information Sciences Institute, January, 1978.

  17. 17.

    McCarthy, John, ‘Towards a mathematical science of computation’, Proceedings of the IFIP Congress, Amsterdam, 1962.

  18. 18.

    McCarthy, John and Painter, J., ‘Correctness of a compiler for arithmetic expressions’, Proceeding of Symposium on Applied Mathematics, American Mathematical Society, 1967.

  19. 19.

    Milner, R. and Weyhrauch, R., ‘Proving compiler correctness in a mechanized logic’, in Machine Intelligence 7, Edinburgh Univ. Press, Edinburgh, Scotland, 1972, pp. 51–70.

  20. 20.

    Milne, R. and Strachey, C., A Theory of Programming Language Semantics, Chapman and Hall, London, 1976.

  21. 21.

    Moore, J S., ‘A mechanically verified language implementation’, Tech. Rept CLI-30, Computational Logic, Inc., September, 1988.

  22. 22.

    Moore, J S., ‘PITON: A verified assembly level language’, Tech. Rept CLI-22, Computational Logic, Inc., June, 1988.

  23. 23.

    Polak, W., Compiler Specification and Verification, Springer-Verlag, Berlin, 1981.

  24. 24.

    Ragland, L. C., ‘A verified program verifier’, PhD Thesis, Univ. of Texas at Austin, 1973.

  25. 25.

    Young, W. D., ‘A verified optimizer for Pico-Piton’, Internal Note 107, December, 1988, Computational Logic, Inc., Austin, Texas.

  26. 26.

    Young, W. D., ‘A verified code generator for a subset of Gypsy’, PhD Thesis, Univ. of Texas at Austin, December, 1988.

Download references

Author information

Rights and permissions

Reprints and Permissions

About this article

Cite this article

Young, W.D. A mechanically verified code generator. J Autom Reasoning 5, 493–518 (1989). https://doi.org/10.1007/BF00243134

Download citation

Key words

  • Automatic theorem proving
  • code generator
  • code verification
  • compiler
  • computational logic
  • correctness
  • program verification
  • programming language
  • semantics
  • system verification