Certifying System Translations Using Higher Order Theorem Provers

Front Cover
Logos Verlag Berlin GmbH, 2009 - Computers - 188 pages
This thesis presents certifying system translations. This is a technique to guarantee the correctness of system translations. When conducting a translation of a system we compare for each translation the original and translated systems and decide whether the translation has been carried out correctly. This decision is based on a certificate generated during the translation process. Thus, we guarantee correctness of translations by verifying each translation run instead of the translation algorithm and its implementation.
 

What people are saying - Write a review

We haven't found any reviews in the usual places.

Contents

Related Work
11
Prerequisites
17
A Framework for Certifying Translations
31
Certifying Code Generation
57
Verifying System Abstractions
113
Evaluation
127
Conclusion
137
B Correctness Formalization in
161
Copyright

Common terms and phrases

Bibliographic information