Translation validation: from Simulink to C

Abstract. Translation validation is a technique for formally establish-ing the semantic equivalence of the source and the target of a code gener-ator. In this work we present a translation validation tool for the Real-Time Workshop code generator that receives as input Simulink models and generates optimized C code.