Deriving correctness properties of compiled code. (English) Zbl 0785.68061
Summary: In 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.
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 03B70 | Logic in computer science |
| 68N20 | Theory of compilers and interpreters |
Keywords:
machine-checked formal verification; object code correctness; compiler correctness; programming logic; HOL systemSoftware:
IBM PC AssemblerReferences:
| [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. · Zbl 0875.68626 |
| [8] | A. Cohn. The notion of proof in hardware verification.Journal of Automated Reasoning, 5:127-138, 1989. · Zbl 0676.68053 · doi:10.1007/BF00243000 |
| [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. · Zbl 0261.68040 · doi:10.1007/BF00289504 |
| [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. · Zbl 0179.23105 · doi:10.1145/363235.363259 |
| [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. · Zbl 0189.50204 |
| [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. · Zbl 0481.68001 |
| [26] | J.S. Moore. A mechanically verified language implementation.Journal of Automated Reasoning, 5:461-492, 1989. |
| [27] | W.D. Young. A mechanically verified code generator.Journal of Automated Reasoning, 5:493-519, 1989. · doi:10.1007/BF00243134 |
| [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. · Zbl 0785.68063 |
| [32] | S. Stepney, D. Whitley, D. Cooper, and C. Grant. A demonstrably correct compiler.Formal Aspects of Computing, 3:58-101, 1991. · Zbl 0712.68025 · doi:10.1007/BF01211435 |
| [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. · Zbl 0544.68006 · doi:10.1002/spe.4380140803 |
| [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. |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
