A Verified Vista Implementation

Front Cover
University of Cambridge, Computer Laboratory, 1993 - Compilers (Computer programs) - 56 pages
0 Reviews
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."

From inside the book

What people are saying - Write a review

We haven't found any reviews in the usual places.

Contents

Contents
1
A Verified Vista Compiler
11
Of What Use is a Verified Compiler Specification?
29

1 other sections not shown

Common terms and phrases

Bibliographic information