Certifying System Translations Using Higher Order Theorem Provers

Beschreibung

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.

Autor*in

Jan Olaf Blech

Themen in »Certifying System Translations Using Higher Order Theorem Provers«

Compiler Softwarekorrektheit Theorembeweisen Verifikation Zertifizierung

Stimmen zu »Certifying System Translations Using Higher Order Theorem Provers«

Details

Link teilen