“Theory and Algorithms for the Generation and Validation of Speculative Loop Optimizations” by Ying Hu, Clark Barrett, and Benjamin Goldberg. In Proceedings of the 2^nd IEEE International Conference on Software Engineering and Formal Methods (SEFM '04), Sep. 2004, pp. 281-289. Beijing, China.
Translation validation is a technique that verifies the results of every run of a translator, such as a compiler, instead of the translator itself. Previous papers by the authors and others have described translation validation for compilers that perform loop optimizations (such as interchange, tiling, fusion, etc), using a proof rule that treats loop optimizations as permutations.
BibTeX entry:
@inproceedings{HBG04,
author = {Ying Hu and Clark Barrett and Benjamin Goldberg},
title = {Theory and Algorithms for the Generation and Validation of
Speculative Loop Optimizations},
booktitle = {Proceedings of the {\it 2^{nd}} IEEE International
Conference on Software Engineering and Formal Methods (SEFM '04)},
pages = {281--289},
publisher = {IEEE Computer Society},
month = sep,
year = {2004},
note = {Beijing, China},
url = {http://theory.stanford.edu/~barrett/pubs/HBG04.pdf}
}
(This webpage was created with bibtex2web.)