Skip to main content
Springer Nature Link
Log in

Deriving correctness properties of compiled code

  • Published:
Formal Methods in System Design Aims and scope Submit manuscript

Abstract

When developing safety-critical software, it is the correctness of the object code that is paramount. However, it is desirable to perform formal verification on the source program. To ensure that correctness results proved about the source program do apply to the object code, the compiler used can be formally verified. However, care must be taken to ensure that the compiler correctness theorem proved is suitable. We have combined a derived programming logic with a verified compiler for a generic subset of the Vista structured assembly language. We show how correctness properties of object code can be formally derived from corresponding correctness properties of the source program which have been proved using the programming logic. Thus we can be sure the results do apply to the object code. The work described has been performed using the HOL system and so is machine-checked.

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

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. MoD: Interim defence standard 00-55 on the procurement of safety critical software in defence equipment, 1991.

  2. P.S. Rajan. Executing HOL specifications: Towards an evaluation semantics for classical higher order logic InHigher Order Logic Theorem Proving and its Applications, L.J.M. Claesen and M.J.C. Gordon, eds. IFIP Transactions A-20, North-Holland, 1993, 527–536.

  3. P. Curzon. Of what use is a verified compiler specification? Technical Report 274, University of Cambridge, Computer Laboratory, 1992.

  4. J. Kershaw. Vista user's guide. Technical Report 401-86, The Royal Signals and Radar Establishment, 1986.

  5. P. Curzon. A verified compiler for a structured assembly language. InProceedings of the 1991 International Workshop on the HOL Theorem Proving System and its Applications, IEEE Computer Society Press, 1992, 253–262.

  6. P. Curzon. Compiler correctness and input/output. InProceedings of the 3rd IFIP Working Conference on Dependable Computing for Critical Applications, Dependable Computing and Fault-Tolerant Computing, Springer-Verlag, 1992.

  7. H.R. Nielson and F. Nielson.Semantics with Applications: A Formal Introduction, Wiley, 1992.

  8. A. Cohn. The notion of proof in hardware verification.Journal of Automated Reasoning, 5:127–138, 1989.

    Google Scholar 

  9. M.J.C. Gordon. Mechanizing programming logics in higher order logic. InCurrent Trends in Hardware Verification and Automated Theorem Proving G. Birtwistle and P. A. Subrahmanyam, eds., Springer-Verlag, 1989, 387–439.

  10. J.J. Joyce. Totally verified systems: Linking verified software to verified hardware. InSpecification, Verification and Synthesis: Mathematical Aspects,, M. Leeser and G. Brown, eds., Springer-Verlag, 1989.

  11. C.A.R. Hoare and N. Wirth. An axiomatic definition of the programming language PASCAL.Acta Informatica, 2:335–355, 1973.

    Google Scholar 

  12. J.J. Joyce. Generic specification of digital hardware. Technical Report 90-27, The University of British Columbia, Department of Computer Science, September, 1990.

  13. C.A.R. Hoare. An axiomatic basis for computer programming.Communications of the ACM, 12(10):576–580,583, October 1969.

    Article  Google Scholar 

  14. P. Curzon. A programming logic for a verified structured assembly language. InLogic Programming and Automated Reasoning, Lecture Notes in Artificial Intelligence, A Voronkov, eds., 624:403–408, Springer-Verlag, 1992.

  15. R.W. Floyd. Assigning meanings to programs. InProceedings of the Symposium on Applied Mathematics, 19:19–32, 1967.

  16. W.D. Maurer. Proving the correctness of a flight-director program for an airborne minicomputer. InProceedings of the ACM SIGMINI/SIGPLAN Interface Meeting on Program Systems in the Small Processor Environment, 1976, 103–108. Appeared as a special issue of SIGPLAN Notice V11(4), April 1976.

  17. W.D. Maurer. An IBM 370 assembly language verifier. InProceedings of the 16th Annual Technical Symposium on Systems and Software: Operational Reliability and Performance Assurance, P.A. Willis eds. ACM, June 1977, 139–146.

  18. P.A. Lamb.A verification condition generator for Intel 8080 microprocessor assembly language programs. PhD thesis, George Washington University, 1982.

  19. D.L. Clutterbuck and B.A. Carré. The verification of low level code.Software Engineering Journal, 97–111, May 1988.

  20. I.M. O'Neill, D.L. Clutterbuck, P.F. Farrow, P.G. Summers, and W.C. Dolman. The formal verification of safety-critical assembly code. InProceedings of the IFAC Symposium on Safety of Computer Control Systems 1988 (Safecomp '88) Safety Related Computers in an Expanding Market, W.D. Ehrenberger eds., 1988.

  21. W.C. Carter, W.H. Joyner, Jr., and D. Brand. Microprogram verification considered necessary. InAFIPS Conference Proceedings 1978 National Computer Conference, Saki P. Ghosh and Leonard Y. Liu eds. 47:657–664, AFIPS Press, June 1978.

  22. P. Curzon. A structured approach to the verification of low level microcode. Technical Report 215, PhD Thesis, University of Cambridge, Computer Laboratory, February, 1991.

  23. R.S. Boyer and Y. Yu. Automated proofs of object code for a commercial microprocessor. InProceedings of the 11th International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence, D. Kapur eds. 607:416–431. Springer-Verlag, 1992.

  24. J.J. Joyce. A verified compiler for a verified microprocessor. Technical Report 167, University of Cambridge, Computer Laboratory, March 1989.

  25. W. Polak.Compiler Specification and Verification, Lecture Notes in Computer Science, 124, Springer-Verlag, 1981.

  26. J.S. Moore. A mechanically verified language implementation.Journal of Automated Reasoning, 5:461–492, 1989.

    Google Scholar 

  27. W.D. Young. A mechanically verified code generator.Journal of Automated Reasoning, 5:493–519, 1989.

    Google Scholar 

  28. T. Simpson, G. Birtwistle, and B. Graham. Some steps towards a verified system.Journal of Software Engineering, May 1993.

  29. D. Martin and R. toal. Case Studies in compiler correctness using HOL. InProceedings of the 1991 International Workshop on the HOL Theorem Proving System and its Applications, IEEE Computer Society Press, 1992.

  30. S. Agerholm. Mechanizing Program verification in HOL. InProceedings of the 1991 International Workshop on the HOL Theorem Proving System and its Applications, IEEE Computer Society Press, 1992, 208–222.

  31. J. von Wright, J. Hekanaho, P. Luostarinen, and T. Långbacka. Mechanising some advanced refinement concepts. In this issue.

  32. S. Stepney, D. Whitley, D. Cooper, and C. Grant. A demonstrably correct compiler.Formal Aspects of Computing, 3:58–101, 1991.

    Google Scholar 

  33. T.F. Melham. Abstraction mechanisms for hardware verification. InVLSI specification, Verification and Synthesis, G. Birtwistle and P.A. Subrahmanyam eds., Kluwer Academic Publishers, 1988, 267–292.

  34. M. Clint and C. Vicent. The use of ghost variables and virtual programming in the documentation and verification of programs.Software Practice and Experience, 14(8):711–737, 1984.

    Google Scholar 

  35. B. Buth, K. Buth, M. Fränzle, B. v. Karger, Y. Lakhneche, H. Langmaack, and M. Müller-Olm. Provably correct compiler development and implementation. InCompiler Construction '92, Lecture Notes in Computer Science, V. Kastens and P. Pfahler, eds., 641:141–155. Springer-Verlag, 1992.

Download references

Author information

Authors and Affiliations

  1. New Museums Site, University of Cambridge Computer Laboratory, Pembroke Street, CB2 3QG, Cambridge, England

    Paul Curzon

Authors
  1. Paul Curzon
    View author publications

    You can also search for this author in PubMed Google Scholar

Rights and permissions

Reprints and permissions

About this article

Cite this article

Curzon, P. Deriving correctness properties of compiled code. Form Method Syst Des 3, 83–115 (1993). https://doi.org/10.1007/BF01383985

Download citation

  • Issue Date:

  • DOI: https://doi.org/10.1007/BF01383985

Keywords

Search

Navigation