We describe CVT - a fully automatic tool for
Code-Validation, i.e. verifying that the target code produced by a code-generator (equivalently, a compiler or
a translator) is a correct implementation of the source
specification. This approach is a viable alternative to a
full formal verification of the codegenerator program,
and has the advantage of not 'freezing' the code generator design after verification.
CVT was developed in the context of the ESPRIT
project SACRES, and validates the translation from State-Mate/Sildex mixed specification into C. The use of novel
techniques based on uninterpreted functions and their
analysis over a BDDrepresented small model enables
us to validate source specifications of several thousands
lines, which represents a typical industrial size safety-critical application.
Software Tools for Technology Transfer, 2