Eingang zum Volltext |
Hinweis zum Urheberrecht
Bitte beziehen Sie sich beim Zitieren dieses Dokumentes immer auf folgende
URL: http://kluedo.ub.uni-kl.de/volltexte/2006/2038/
Gawkowski, Marek Jerzy ; Blech, Jan Olaf ; Poetzsch-Heffter, Arnd
Certifying Compilers based on Formal Translation Contracts
| PDF (Portable Document Format): |
| |
| DjVu: |
|
Kurzfassung in englisch
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.
| Freie Schlagwörter (englisch): | Certifying Compilers, Translation Validation | |
| Reihe: | Interne Berichte | |
| Band: | 355 | |
| DDC-Sachgruppe: | Informatik | |
| Sonstige beteiligte Institution: | Technische Universität Kaiserslautern | |
| Dokumentart: | Preprint (Vorabdruck) | |
| Sprache: | englisch | |
| Erstellungsjahr: | 2006 | |
| Publikationsdatum: | 25.11.2006 |
Fragen und Anregungen an kluedo@ub.uni-kl.de