Abstract
The paper presents an approach to the translation validation of an optimizing compiler which translates synchronous C programs into machine code programs. Being synchronous means that both source and target programs are loop free. This enables representation of each of these programs by a single state transformer, and verification of the translation correctness is based on comparison of the source and target state transformers. The approach has been implemented on a tool called MCVT which is also described. © Springer-Verlag 2004.
Cite
CITATION STYLE
Gordin, I., Leviathan, R., & Pnueli, A. (2004). Validating the translation of an industrial optimizing compiler. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 3299, 230–247. https://doi.org/10.1007/978-3-540-30476-0_21
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
