Certifying Compilers based on Formal Translation Contracts

  • A translation contract is a binary predicate corrTransl(S,T) for source programs S and target programs T. It precisely specifies when T is considered to be a correct translation of S. A certifying compiler generates --in addittion to the target T-- a proof for corrTransl(S,T). Certifying compilers are important for the development of safety critical systems to establish the behavioral equivalence of high-level programs with their compiled assembler code. In this paper, we report on a certifying compiler, its proof techniques, and the underlying formal framework developed within the proof assistent Isabelle/HOL. The compiler uses a tiny C-like language as input, has an optimization phase, and generates MIPS code. The underlying translation contract is based on a trace semantics. We investigate design alternatives and discuss our experiences.

Volltext Dateien herunterladen

Metadaten exportieren

  • Export nach Bibtex
  • Export nach RIS

Weitere Dienste

Teilen auf Twitter Suche bei Google Scholar
Metadaten
Verfasserangaben:Marek Jerzy Gawkowski, Jan Olaf Blech, Arnd Poetzsch-Heffter
URN (Permalink):urn:nbn:de:hbz:386-kluedo-14698
Schriftenreihe (Bandnummer):Interner Bericht des Fachbereich Informatik (355)
Dokumentart:Preprint
Sprache der Veröffentlichung:Englisch
Jahr der Fertigstellung:2006
Jahr der Veröffentlichung:2006
Veröffentlichende Institution:Technische Universität Kaiserslautern
Beteiligte Körperschaft:Technische Universität Kaiserslautern
Datum der Publikation (Server):25.11.2006
Freies Schlagwort / Tag:Certifying Compilers; 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 $