Compiler Verification for C0

Martin Strecker


This paper describes formalisations of a type-safe fragment of the C programming language (called C0) and of the DLX assembly language. It then presents the definition and correctness proof of a substantial fragment of a C0-to-DLX compiler, carried out in the proof assistant Isabelle.
 Online Copy

Available as PDF
 BibTeX Entry

  author = 	 {Martin Strecker},
  title = 	 {Compiler Verification for {C0} (intermediate report)},
  institution =  {Universit{\'e} Paul Sabatier},
  year = 	 2005,
  address =	 {Toulouse},
  month =	 {April}

Last modified: Thu Jul 30 10:55:26 CEST 2009