Dependable Computing for Critical Applications 3 pp 189-209 | Cite as

# Compiler Correctness and Input/Output

Conference paper

## Abstract

We describe the formal machine-checked verification of a compiler from a subset of the Vista structured assembly language to the flat assembly language Visa. In particular, we describe the problems associated with input and output commands. We present an oracle based model of I/O. We show how this model can be incorporated into both the relational semantics of Vista and the interpreter semantics of Visa. We illustrate how the compiler correctness theorem proved is sufficient to deduce correctness properties of compiled code from properties of the original program.

## Keywords

Semantic Relation Target Language Assembly Language High Order Logic Total Correctness
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

## Preview

Unable to display preview. Download preview PDF.

## References

- [1]W. R. Bevier, Jr., W. A. Hunt, W. D. Young. Towards verified execution environments.
*Proc. of the 1987 IEEE Symp. on Security and Privacy*, 1987.Google Scholar - [2]A. Cohn. A proof of correctness of the Viper microprocessor: The first level.
*VLSI Specification, Verification and Synthesis*, G. Birtwistle, P. A. Subrahmanyam Eds., Kluwer Academic Publishers, 1988, pp. 1-91.Google Scholar - [3]A. Cohn. Correctness properties of the Viper block model: The second level.
*Current Trends in Hardware Verification and Automated Theorem Proving*, G. Birtwistle, P. A. Subrahmanyam Eds., Springer-Verlag, 1989, pp. 27-72.Google Scholar - [4]W. J. Cullyer. Implementing safety critical systems: The Viper Microprocessor.
*VLSI Specification, Verification and Synthesis*, G. Birtwistle, P. A. Subrahmanyam Eds., Kluwer Academic Publishers, 1988, pp. 1-25.Google Scholar - [5]P. Curzon. A verified compiler for a structured assembly language.
*Proc. of the 1991 Int. Workshop on the HOL Theorem Proving System and its Applications*, IEEE Computer Society Press, 1992, pp. 253-262.Google Scholar - [6]P. Curzon. A programming logic for a verified structured assembly language.
*Logic Programming and Automated Reasoning*, A. Voronkov Ed., Lecture Notes in Artificial Intelligence Vol. 624, Springer-Verlag, 1992, pp. 403-408.Google Scholar - [7]P. Curzon. Deriving correctness properties of compiled code.
*Proc. of the 1992 Int. Workshop on Higher Order Logic Theorem Proving and its Applications*, L. Claesen, M. Gordon Eds., 1992.Google Scholar - [8]J. Despeyroux. Proof of translation in natural semantics.
*IEEE Symp. on Logic in Computer Science*, 1986, pp. 193-205.Google Scholar - [9]M. J. C. Gordon. Mechanizing programming logics in higher order logic.
*Current Trends in Hardware Verification and Automated Theorem Proving*, G. Birtwistle, P. A. Subrahmanyam Eds., Springer-Verlag, 1989, pp. 387-439.Google Scholar - [10]M. J. C. Gordon, T. F. Melham Eds.
*Introduction to HOL: A Theorem Proving Environment for Higher Order Logic*. Cambridge University Press, 1992.Google Scholar - [11]C. A. R. Hoare, N. Wirth. An axiomatic definition of the programming language PASCAL.
*Acta Informatica*, Vol. 2, 1973, pp. 335–355.CrossRefGoogle Scholar - [12]C. A. R. Hoare.
*Communicating Sequential Processes*. Prentice Hall Int., 1985.Google Scholar - [13]J. J. Joyce. A verified compiler for a verified microprocessor.
*Technical Report 167*, University of Cambridge, Computer Laboratory, March 1989.Google Scholar - [14]J. J. Joyce. Generic specification of digital hardware.
*Technical Report 90-27*, The University of British Columbia, Department of Computer Science, September 1990.Google Scholar - [15]J. J. Joyce. Private communication. 1990.Google Scholar
- [16]J. Kershaw. Vista user’s guide.
*Technical Report 401-86*, RSRE, 1986.Google Scholar - [17]D. Martin, R. Toal. Case studies in compiler correctness using HOL.
*Proc. of the 1991 Int. Workshop on the HOL Theorem Proving System and its Applications*, IEEE Computer Society Press, 1992, pp 242-252.Google Scholar - [18]J. McCarthy, J. Painter. Correctness of a compiler for arithmetic expressions.
*Proc. of Symp. in Applied Mathematics*, J. T. Schwartz Ed., Vol. XIX, 1966, pp. 33-41.Google Scholar - [19]T. F. Melham. Abstraction mechanisms for hardware verification.
*VLSI Specification, Verification and Synthesis*, G. Birtwistle and P. A. Subrahmanyam Eds., Kluwer Academic Publishers, 1988, pp. 267-292.Google Scholar - [20]J. S. Moore. A mechanically verified language implementation.
*Journal of Automated Reasoning*, Vol. 5, 1989, pp. 461–492.Google Scholar - [21]G. D. Plotkin. A structural approach to operational semantics.
*Technical report*, University of Aarhus, Denmark, Computer Science Department, 1981.Google Scholar - [22]W. Polak. Compiler Specification and Verification.
*Lecture Notes in Computer Science Vol. 124*, Springer-Verlag, 1981.Google Scholar - [23]T. G. Simpson. Design and verification of IFL: a wide-spectrum intermediate functional language.
*Technical Report 91/440/24*, The University of Calgary, Department of Computer Science, July 1991.Google Scholar - [24]S. Stepney, D. Whitley, D. Cooper, C. Grant. A demonstrably correct compiler.
*Formal Aspects of Computing*, Vol. 3, 1991, pp. 58–101.MATHCrossRefGoogle Scholar - [25]W. D. Young. A mechanically verified code generator.
*Journal of Automated Reasoning*, Vol. 5, 1989, pp. 493–519.CrossRefGoogle Scholar

## Copyright information

© Springer-Verlag Wien 1993