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.

Export metadata

  • Export Bibtex
  • Export RIS

Additional Services

Share in Twitter Search Google Scholar
Metadaten
Author:Marek Jerzy Gawkowski, Jan Olaf Blech, Arnd Poetzsch-Heffter
URN (permanent link):urn:nbn:de:hbz:386-kluedo-14698
Serie (Series number):Interner Bericht des Fachbereich Informatik (355)
Document Type:Preprint
Language of publication:English
Year of Completion:2006
Year of Publication:2006
Publishing Institute:Technische Universität Kaiserslautern
Contributing Corporation:Technische Universität Kaiserslautern
Tag:Certifying Compilers; Translation Validation
Faculties / Organisational entities:Fachbereich Informatik
DDC-Cassification:004 Datenverarbeitung; Informatik

$Rev: 12793 $