Refine
Year of publication
- 2006 (1)
Document Type
- Preprint (1)
Language
- English (1)
Has Fulltext
- yes (1)
Keywords
- Certifying Compilers (1) (remove)
Faculty / Organisational entity
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.