Wed, 3 Feb 1993 12:40:50 GMT

Related articles |
---|

Looking for references on correctness concerns in compilation martinc@cs.unc.edu (1993-02-02) |

Re: Looking for references on correctness concerns in compilation pc@cl.cam.ac.uk (1993-02-03) |

Newsgroups: | comp.compilers |

From: | pc@cl.cam.ac.uk (Paul Curzon) |

Keywords: | theory, bibliography |

Organization: | Cambridge Automated Reasoning Group |

References: | 93-02-026 |

Date: | Wed, 3 Feb 1993 12:40:50 GMT |

*> I'm at work on a project involving the development of "trusted compilers"*

*> --- compilers for which there is a strong guarantee of correct*

*> compilation. I would like to hear from anyone who is involved in*

*> something similar; in particular, I'm interested in finding research that*

*> relates to provably confirming the results of optimizations and code*

*> generation.*

I have been working on a project (soon to finish) on the mechanical formal

verification of a code generator using the HOL system. The language in

question is Vista which is a structured assembly language for the Viper

microprocessor. I have also looked at ways of executing a verified

compiler specification securely using a theorem prover, and formally

connecting a compiler proof with a programming logic. There has also been

other work done here at Cambridge. The journal of automated reasoning had

a special issue on the Boyer-Moore system verification work a few years

back which you should check out. Polak's work is also worth looking at.

Jeff Joyce's tech report has quite an good overview of early compiler

verification work. There has also been a vast amount of work done on the

ProCos project at various institutions. I can send you copies of my papers

or other Cambridge tech. reports if you are interested. If it would be

useful I could send you a copy of my full bibliography of compiler

verification literature.

Paul Curzon

-----------

@TechReport{CamilleriJ91a,

author = "Juanito Camilleri",

title = "Symbolic Compilation and Execution of Programs by Proof: A

Case study in {HOL}",

institution = "University of Cambridge, Computer Laboratory",

year = "1991",

number = "240",

month = dec,

*}*

@InProceedings{Curzon91,

author = "Paul Curzon",

title = "A Verified Compiler for a Structured Assembly Language",

booktitle = "Proceedings of the 1991 International Workshop on the {HOL}

Theorem Proving System and its Applications",

year = "1992",

OPTeditor = "Myla Archer and Jeffrey J. Joyce and Karl N. Levitt and

Phillip J. Windley",

publisher = "{IEEE} Computer Society Press",

OPTnote = "A compiler for a small structured assembly language schema

based on Vista is verified using HOL. It compiles to a flat

assembly language. Properties of safety and liveness are

defined and it is suggested that proofs of source language

programs could be mapped to proofs of target language

programs.The compiler can be executed using the theorem

prover."

*}*

@InProceedings{Curzon92DCCA,

key = "Curzon92b",

author = "Paul Curzon",

title = "Compiler Correctness and Input/Output",

booktitle = "Proceedings of the 3rd {IFIP} Working Conference on

Dependable Computing for Critical Applications",

year = "1992",

publisher = "Springer-Verlag",

series = "Dependable Computing and Fault-Tolerant Computing",

OPTnote = "The proof of correctness for the Vista compiler is extended

to include IO commands. An oracle model of IO is used in the

semantics, and it is shown that this does not hinder the

proof."

*}*

@InProceedings{Curzon92LPAR,

key = "Curzon92a",

author = "Paul Curzon",

title = "A Programming Logic For a Verified Structured Assembly

Language",

booktitle = "Logic Programming and Automated Reasoning",

year = "1992",

editor = "A. Voronkov",

pages = "403-408",

publisher = "Springer-Verlag",

volume = "624",

series = "Lecture Notes in Artificial Intelligence",

OPTnote = "A programming logic of total correctness for a subset of the

structured assembly language Vista is developed. It includes

IO commands. Assertions about IO behaviour are made in the

preconditions as predictions. The logic has been derived from

a relational semantics in HOL."

*}*

@InProceedings{Curzon92HOL,

author = "Paul Curzon",

title = "Deriving Correctness Properties of Compiled Code",

booktitle = "International Workshop on Higher

Order Logic Theorem Proving and its Applications",

year = "1992",

editor = "L. Claesen and M. Gordon",

OPTnote = "A derived programming logic is combined with a verified

implementation of Vista. This allows total correctness proofs

to be performed on high level programs, and total correctness

theorems about compiled code can be automatically obtained."

*}*

@TechReport{Curzon92WhyTR,

author = "Paul Curzon",

title = "Of What Use is a Verified Compiler Specification?",

institution = "University of Cambridge, Computer Laboratory",

year = "1992",

number = "274",

OPTnote = "Splitting a proof into implementation correctness and

Specification correctness. A secure way of executing a

verified specification by proof. Bootstrapping a

verified compiler in a low level language, without first

having a verified compiler implementation

available by ftp from ftp.cl.cam.ac.uk in the

directory hvg/papers. It is in the file WhyCompilerSpec.ps.Z"

*}*

@InProceedings{Joyce89b,

author = "Jeffrey J. Joyce",

title = "Totally Verified Systems: Linking Verified Software to

Verified Hardware",

booktitle = "Specification, Verification and Synthesis: Mathematical

Aspects",

year = "1989",

editor = "M. Leeser and G. Brown",

publisher = "Springer-Verlag",

*}*

@TechReport{Joyce89,

author = "Jeffrey J. Joyce",

title = "A Verified Compiler for a Verified Microprocessor",

institution = "University of Cambridge, Computer Laboratory",

year = "1989",

number = "167",

month = mar,

}

@Book{Polak81,

author = "Wolfgang Polak",

title = "Compiler Specification and Verification",

publisher = "Springer-Verlag",

year = "1981",

OPTeditor = "G. Goos and J. Hartmanis",

volume = "124",

series = "Lecture Notes in Computer Science",

*}*

@Article{StrotherMoore88,

author = "J. Strother Moore",

title = "A Mechanically Verified Language Implementation",

journal = "Journal of Automated Reasoning",

year = "1989",

volume = "5",

pages = "461--492",

*}*

@Article{Young89,

author = "William D. Young",

title = "A Mechanically Verified Code Generator",

journal = "Journal of Automated Reasoning",

year = "1989",

volume = "5",

pages = "493--519",

*}*

--

Paul Curzon | Tel: +44-223-334688

University of Cambridge | Fax: +44-223-334678

Computer Laboratory |

New Museums Site |

Pembroke Street | Email: pc@cl.cam.ac.uk

Cambridge CB2 3QG |

United Kingdom |

--

Post a followup to this message

Return to the
comp.compilers page.

Search the
comp.compilers archives again.