“TVOC: A Translation Validator for Optimizing Compilers” by Clark Barrett, Yi Fang, Ben Goldberg, Ying Hu, Amir Pnueli, and Lenore Zuck. In Proceedings of the 17^th International Conference on Computer Aided Verification (CAV '05), (Kousha Etessami and Sriram K. Rajamani, eds.), July 2005, pp. 291-295. Edinburgh, Scotland.
We describe a tool called TVOC, that uses the translation validation approach to check the validity of compiler optimizations: for a given source program, TVOC proves the equivalence of the source code and the target code produced by running the compiler. There are two phases to the verification process: the first phase verifies loop transformations using the proof rule permute; the second phase verifies structure-preserving optimizations using the proof rule Validate. Verification conditions are validated using the automatic theorem prover CVC Lite.
BibTeX entry:
@inproceedings{BFG+05,
author = {Clark Barrett and Yi Fang and Ben Goldberg and Ying Hu and
Amir Pnueli and Lenore Zuck},
editor = {Kousha Etessami and Sriram K. Rajamani},
title = {{TVOC}: A Translation Validator for Optimizing Compilers},
booktitle = {Proceedings of the {\it 17^{th}} International Conference
on Computer Aided Verification (CAV '05)},
series = {Lecture Notes in Computer Science},
volume = {3576},
pages = {291--295},
publisher = {Springer-Verlag},
month = jul,
year = {2005},
note = {Edinburgh, Scotland},
url = {http://theory.stanford.edu/~barrett/pubs/BFG+05.pdf}
}
(This webpage was created with bibtex2web.)