Compiler Validation with Automated Decision Procedures

Dr. Clark Barrett

Computer Science Department
New York University

Translation validation is an approach pioneered at NYU for validating the 
output of optimizing compilers.  Rather than verifying the compiler itself, 
translation validation mandates that every run of the compiler generate a 
formal proof that the produced target code is a correct implementation of the 
source code.  Thus, every run of the compiler generates a set of verification 
conditions that must be discharged by a theorem prover.  Our theorem prover of 
choice is CVC Lite, a tool being developed jointly at NYU and Stanford 
University, building on the success of its predecessors, SVC and CVC. 

This talk will give an overview of CVC Lite and its use in translation 
validation.  We will then discuss some recent work on speculative 
optimizations, optimizations which are only correct under certain conditions 
which cannot be validated at compile time.  We show how CVC Lite can be used to automatically generate run-time tests to allow the safe use of such speculative 
optimizations.