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.

Download full text files

Export metadata

Additional Services

Search Google Scholar
Author:Marek Jerzy Gawkowski, Jan Olaf Blech, Arnd Poetzsch-Heffter
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
Date of the Publication (Server):2006/11/25
Tag:Certifying Compilers; Translation Validation
Faculties / Organisational entities:Kaiserslautern - Fachbereich Informatik
DDC-Cassification:0 Allgemeines, Informatik, Informationswissenschaft / 004 Informatik
Licence (German):Standard gemäß KLUEDO-Leitlinien vor dem 27.05.2011