Certifying System Translations Using Higher Order Theorem Provers
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.
A Framework for Certifying Translations
Certifying Code Generation
Verifying System Abstractions
B Correctness Formalization in
abstract store absval accesses in variable algorithm assertion to rewrite aval store bisimulation certiﬁcate certifying translations checker predicates checker semantics checking coalgebraic Compiler Optimization computed Correctness Criterion correctness proof CorrectSteps criteria datatype deﬁned deﬁnition deterministic diﬀerent evalinstruction evaloperand L G locvals evaluate succeeding MIPS ﬁrst formalized framework fulﬁll gvals lvals iﬀ implementation initial instantiated intermediate language Isabelle Isabelle/HOL Kripke structures L G locvals globvals labeled transition systems lemma look-up lop,opl,op2 lop.opl mem MemMap memorycorrespondence MIPS code MIPS state representation mkilstate model checking natural numbers nexti(s nextstate non-silent transition notion of correctness operand operational semantics output phase prevlabel procedure program counters correspond programcounter correspondence proof script ProofCode properties representation evaluate succeeding representation splitgoalintosubgoals rewrite variable accesses Section simulation relation state.(globvals state.(output state.(pid state.(stack store representation qed system abstractions theorem prover thesis tlnextn tlstatement transition function transition relation trusted computing base variable mapping variable store representation varvals veriﬁcation