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.
Author: | Marek Jerzy Gawkowski, Jan Olaf Blech, Arnd Poetzsch-Heffter |
---|---|
URN: | 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 |
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): |