MCVT

MCVT, machine code validation tool, is a translation validation tool, which validates synchronous C programs. It uses a proof procedure, together with the annotation algorithm and additional heuristics, to automatically produce verification conditions. The verification conditions are formulas of decidable logic theories. MCVT uses CVC, a Cooperating Validity Checker, developed at Stanford University, (CVC) to establish the validity of the verification conditions, and thus the correctness of the translation.

This tool was developed as part of the SafeAir-II project of IST (Information Society Technologies program of the European Union).

The paper "Validating Translation of an Industrial Optimizing Compiler", by I. Gordin, R. Leviathan, A. Pnueli (ATVA 2004 proceedings as LNCS, Springer-Verlag), describes the tool.

A more comprehensive description can be find in "Validation of Translation to Optimized Machine Code" by Raya Leviathan. Ph.D. Thesis, Department of Computer Science & Applied Mathematics, Weizmann Institute of Science" - book.pdf .

To install MCVT, uncompress the file MCVT_DIR.zip, then read MCVT_DIR/docs/manual.pdf. The zip file contains both Linux and Solaris versions. Please read cvc license file (MCVT_DIR/license/LICENSE) before doing any use of the software.

For any questions or comments, please e-mail Raya Leviathan.

Dept. of Computer Science and Applied Math
The Weizmann Institute of Science
Rehovot 76100, Israel
TelePhone: +972-8-934-3434
Telefax: +972-8-934-4122
To comment on this service, send feedback to the Nir Piterman