Technical reports

Totally verified systems:
linking verified software to verified hardware

Jeffrey J. Joyce

September 1989, 25 pages

DOI: 10.48456/tr-178

Abstract

We describe exploratory efforts to design and verify a compiler for a formally verified microprocessor as one aspect of the eventual goal of building totally verified systems. Together with a formal proof of correctness for the microprocessor this yields a precise and rigorously established link between the semantics of the source language and the execution of compiled code by the fabricated microchip. We describe in particular: (1) how the limitations of real hardware influenced this proof; and (2) how the general framework provided by higher order logic was used to formalize the compiler correctness problem for a hierarchically structured language.

Full text

PDF (1.5 MB)

BibTeX record

@TechReport{UCAM-CL-TR-178,
  author =	 {Joyce, Jeffrey J.},
  title = 	 {{Totally verified systems: linking verified software to
         	   verified hardware}},
  year = 	 1989,
  month = 	 sep,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-178.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-178},
  number = 	 {UCAM-CL-TR-178}
}