A Verified Vista ImplementationAbstract: "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." |
Contents
Introduction | 1 |
A Verified Vista Compiler | 11 |
Of What Use is a Verified Compiler Specification? | 29 |
1 other sections not shown
Common terms and phrases
abstract specification APPEND application programs approach arg1 arg2 Bootstrapping code produced command comparison operations compiled code CompileProgram compiler correctness proof compiler correctness theorem compiler implementation compiler specification considered correctness properties correctness statement corresponding declarations defined definitions derived inference rule 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 oracle 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 theorem prover tool total correctness translation to ML type variables v1 x v2 validation verified compiler VIPER microprocessor VIPER1rep Visa compiler Visa to Kaa Vista programmer VistaSemantics Vlist