Technical reports

A verified Vista implementation

Paul Curzon

September 1993, 56 pages

DOI: 10.48456/tr-311

Abstract

We describe the formal verification of a simple compiler using the HOL theorem proving system. The language and microprocessor considered are a subset of the structured assembly language Vista, and the Viper microprocessor, respectively. We describe how our work is directly applicable to a family of languages and compilers and discuss how the correctness theorem and verified compiler fit into a wider context of ensuring that object code is correct. We first show how the compiler correctness result can be formally combined with a proof system for application programs. We then show how our verified compiler, despite not being written in a traditional programming language, can be used to produce compiled code. We also discuss how a dependable implementation might be obtained.

Full text

PDF (5.6 MB)

BibTeX record

@TechReport{UCAM-CL-TR-311,
  author =	 {Curzon, Paul},
  title = 	 {{A verified Vista implementation}},
  year = 	 1993,
  month = 	 sep,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-311.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-311},
  number = 	 {UCAM-CL-TR-311}
}