Skip to content (access key 's')
Logo of Technion
Logo of CS Department
Logo of CS4People

The Taub Faculty of Computer Science Events and Talks

Translation validation: from Simulink to C.
event speaker icon
Michael Riabzev (M.Sc. Thesis Seminar)
event date icon
Wednesday, 18.03.2009, 14:00
event location icon
Taub 601
event speaker icon
Advisor: Dr. Ofer Strichman
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.