“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.)