The Taub Faculty of Computer Science Events and Talks

Translation validation is a technique for formally establishing the semantic equivalence of a source and a target of a code generator/compiler. 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. The lecture will begin with a demonstration of the Simulink models format and automatically generated C code. It will then focus on the verification condition that is required for establishing the equivalence, as well as the tool TVS which was built as part of the thesis for extracting this condition from Simulink models and C code.