Translation Validation: From Simulink to C

被引：0

作者：

Ryabtsev, Michael ^{[1
]}

Strichman, Ofer ^{[1
]}

机构：

[1] Technion Israel Inst Technol, IE, Haifa, Israel

来源：

COMPUTER AIDED VERIFICATION, PROCEEDINGS | 2009年 / 5643卷

关键词：

D O I：

暂无

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

Translation validation is a technique for formally establishing the semantic equivalence of the source and the target of a code generator. 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.

引用

页码：696 / 701

页数：6

共 9 条

[1]

[Anonymous], 2006, YICES SMT SOLVER

[2] EFFICIENTLY COMPUTING STATIC SINGLE ASSIGNMENT FORM AND THE CONTROL DEPENDENCE GRAPH [J].

CYTRON, R ;

FERRANTE, J ;

ROSEN, BK ;

WEGMAN, MN ;

ZADECK, FK .

ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1991, 13 (04) :451-490

[3]

MATHWORKS T, SIMULINK 7 USER GUID

[4]

MATHWORKS T, SIMULINK GETTING STA

[5]

NECULA GC, 2000, PLDI 2000

[6] The Code Validation Tool (CVT) Automatic verification of a compilation process [J].

A. Pnueli ;

O. Shtrichman ;

M. Siegel .

International Journal on Software Tools for Technology Transfer, 1998, 2 (2) :192-201

[7]

Pnueli A, 1998, LECT NOTES COMPUT SC, V1443, P235, DOI 10.1007/BFb0055057

[8]

PNUELI A, 1997, TRANSLATION VALIDATI

[9]

RYABTSEV M, 2009, IEIS200901

← 1 →