TY - GEN
T1 - Translation validation of loop optimizations and software pipelining in the TVOC framework
T2 - 17th International Static Analysis Symposium, SAS 2010
AU - Goldberg, Benjamin
N1 - Copyright:
Copyright 2010 Elsevier B.V., All rights reserved.
PY - 2010
Y1 - 2010
N2 - Translation validation (TV) is the process of proving that the execution of a translator has generated an output that is a correct translation of the input. When applied to optimizing compilers, TV is used to prove that the generated target code is a correct translation of the source program being compiled. This is in contrast to verifying a compiler, i.e. ensuring that the compiler will generate correct target code for every possible source program - which is generally a far more difficult endeavor. This paper reviews the TVOC framework developed by Amir Pnueli and his colleagues for translation validation for optimizing compilers, where the program being compiled undergoes substantional transformation for the purposes of optimization. The paper concludes with a discussion of how recent work on the TV of software pipelining by Tristan & Leroy can be incorporated into the TVOC framework.
AB - Translation validation (TV) is the process of proving that the execution of a translator has generated an output that is a correct translation of the input. When applied to optimizing compilers, TV is used to prove that the generated target code is a correct translation of the source program being compiled. This is in contrast to verifying a compiler, i.e. ensuring that the compiler will generate correct target code for every possible source program - which is generally a far more difficult endeavor. This paper reviews the TVOC framework developed by Amir Pnueli and his colleagues for translation validation for optimizing compilers, where the program being compiled undergoes substantional transformation for the purposes of optimization. The paper concludes with a discussion of how recent work on the TV of software pipelining by Tristan & Leroy can be incorporated into the TVOC framework.
UR - http://www.scopus.com/inward/record.url?scp=78149250008&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=78149250008&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-15769-1_3
DO - 10.1007/978-3-642-15769-1_3
M3 - Conference contribution
AN - SCOPUS:78149250008
SN - 3642157688
SN - 9783642157684
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 6
EP - 21
BT - Static Analysis - 17th International Symposium, SAS 2010, Proceedings
Y2 - 14 September 2010 through 16 September 2010
ER -