Loading...
Please wait, while we are loading the content...
Similar Documents
The Verified Compilation of Vista Programs (1994)
| Content Provider | CiteSeerX |
|---|---|
| Author | Curzon, Paul |
| Abstract | We describe the formal machine-checked verification of a simple compiler specification 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. Our work is directly applicable to a family of languages and compilers. We discuss how the correctness theorem and verified compiler fit into a wider context of ensuring that object code is correct. We show how the compiler correctness result can be formally combined with a proof system for application programs. We have implemented a tool that executes the verified compiler specification using formal proof. We also suggest a way that a dependable implementation might be obtained. |
| File Format | |
| Language | English |
| Publisher Date | 1994-01-01 |
| Access Restriction | Open |
| Subject Keyword | Verified Compilation Vista Program Object Code Simple Compiler Specification Formal Proof Application Program Verified Compiler Specification Compiler Correctness Result Dependable Implementation Wider Context Correctness Theorem Formal Machine-checked Verification Viper Microprocessor Proof System Hol Theorem Verified Compiler Fit Assembly Language Vista |
| Content Type | Text |
| Resource Type | Technical Report |