Re: Looking for references on correctness concerns in compilation

> 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 |
--

Return to the comp.compilers page.
Search the comp.compilers archives again.