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} }