A Verified Vista Implementation
University of Cambridge, Computer Laboratory, 1993 - Compilers (Computer programs) - 56 pages
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."
What people are saying - Write a review
We haven't found any reviews in the usual places.
A Verified Vista Compiler
Of What Use is a Verified Compiler Specification?
1 other sections not shown
abstract specification AbstractCompilerSpec APPEND application programs approach arg2 argl Bootstrapping code produced combined command CompareVisaKaaStates comparison operations compiled code compiled programs compiler correctness proof compiler correctness theorem compiler implementation compiler specification considered correctness properties correctness statement corresponding declarations defined definitions derived inference rule environment error example execution by proof formal specification formally verified function give given higher-order logic I/O behaviour initial input insecure compiler instantiated instructions Kaa compiler microcode multiplication program Nuprl object code obtained output performed postcondition pretty-printers procedure program counter programming language proved rep env penv representation tuple secure semantic relation semantically embedded SemCommand source and target source language source program Standard ML structured assembly language syntax target code target language target machine techniques testing theorem prover tool total correctness type variables validation verified compiler VIPER microprocessor VIPERlrep Visa Vista compiler Vista programmer vl x v2 Vlist