The Compiler Validation Project:
Developing tools for proving the correctness of compilation.

   

Early Translation Validation:

Translation Validation: From SIGNAL to C, A. Pnueli, M. Siegel, and O. Shtrichman, In "Correct System Design", E.-R. Olderog and B. Steffen eds., LNCS State-of-the-Art Survey, volume 1710,Springer Verlag, 1999, pp. 231--255.

The Code Validation Tool (CVT)- Automatic Verification of a compilation process, A. Pnueli, M. Siegel, and O. Shtrichman, In "Software Tools for Technology Transfer", Volume 2, 1999.

Current Papers:

Validation of Optimizing Compilers, L. Zuck, A. Pnueli, and R. Leviathan, Weizmann Institute of Science Report MCS01-12, August 2001.

VOC: A Translation Validator for Optimizing Compilers, L. Zuck, A. Pnueli, Y.Fang, and B. Goldberg, In Internation workshop on Compiler Optimization meets Compiler Verificaiton (COCV), April 2002.

Translation and Run-Time Validation for Optimized Code, L. Zuck, A. Pnueli, Y.Fang, B. Goldberg, and Y.Hu. In the Workshop on Run-Time Verification (RV), July 2002.

VOC: A Methodology for Translation Validation of Optimizing Compilers , L. Zuck, A. Pnueli, Y.Fang, and B. Goldberg. To appear in the Journal of Universal Computer Science.