Mechanical Verification of Compiler Correctness
David W.J. Stringer-Calvert
DPhil Thesis, Department of Computer Science, University of York, UK.
Accepted March 1998.
Abstract
A large investment is made in the development, testing, validation and verification of
source code for critical applications. But there remains a semantic gap between
the source code produced and the object code which is executed. Standards for the
development of critical systems recognize this, and mandate either the use of a
trusted compiler (one that has been proven to produce correct object code) or the
demonstration that the object code is a correct refinement of the source
code (a lengthy and complex process).
This thesis examines:
- the extent to which tool support is an essential ingredient in proofs of compiler
correctness;
- the extent to which these proofs may be automated;
- the relationship between the complexity of the source language and the proof effort required;
- the scalability of a mechanical method of compiler verification.
To do this, we present the development of the proof of correctness of a compiler
for a small imperative language Tosca, targeted at an imaginary assembler Aida.
The work presented here is an extension of the Z specification and hand proof presented in Stepney's
book
``High Integrity Compilation --- A Case Study'', recasting the specification and proofs
within the framework of the PVS
specification and verification system from SRI International.
We also assess the lessons learnt in the translation of a hand treatment
of the problem in a partial logic, to an automatic treatment in a total logic with
a richly expressive type system; from hand proof to automatic checking, and the
inter-relationship between the specification and the ability to automate the proof process.
Available as
PostScript from The University of York (best for European download).
And a local copy here at SRI-CSL (best for US download).
BibTeX Entry
@phdthesis{davesc-thesis,
TITLE = {Mechanical Verification of Compiler Correctness},
AUTHOR = {David W.J. Stringer-Calvert},
SCHOOL = {Department of Computer Science, University of York},
MONTH = mar,
YEAR = 1998
}
Return to my publications page
Return to the Computer Science Laboratory home page
Dave Stringer-Calvert