On Certifying Code Generation

  • Guaranteeing correctness of compilation is a ma jor precondition for correct software. Code generation can be one of the most error-prone tasks in a compiler. One way to achieve trusted compilation is certifying compilation. A certifying compiler generates for each run a proof that it has performed the compilation run correctly. The proof is checked in a separate theorem prover. If the theorem prover is content with the proof, one can be sure that the compiler produced correct code. This paper presents a certifying code generation phase for a compiler translating an intermediate language into assembler code. The time spent for checking the proofs is the bottleneck of certifying compilation. We exhibit an improved framework for certifying compilation and considerable advances to overcome this bottleneck. We compare our implementation featuring the Coq theorem prover to an older implementation. Our current implementation is feasible for medium to large sized programs.

Volltext Dateien herunterladen

Metadaten exportieren

  • Export nach Bibtex
  • Export nach RIS

Weitere Dienste

Teilen auf Twitter Suche bei Google Scholar
Metadaten
Verfasserangaben:Jan Olaf Blech
URN (Permalink):urn:nbn:de:hbz:386-kluedo-15086
Schriftenreihe (Bandnummer):Interner Bericht des Fachbereich Informatik (366)
Dokumentart:Bericht
Sprache der Veröffentlichung:Englisch
Jahr der Fertigstellung:2007
Jahr der Veröffentlichung:2007
Veröffentlichende Institution:Technische Universität Kaiserslautern
Datum der Publikation (Server):03.12.2007
Freies Schlagwort / Tag:Coq; compiler; theorem prover; translation validation
Fachbereiche / Organisatorische Einheiten:Fachbereich Informatik
DDC-Sachgruppen:0 Informatik, Informationswissenschaft, allgemeine Werke / 00 Informatik, Wissen, Systeme / 004 Datenverarbeitung; Informatik
Lizenz (Deutsch):Standard gemäß KLUEDO-Leitlinien vor dem 27.05.2011

$Rev: 13581 $