The VeriTech framework for translation is described. A system being analyzed is seen as a collection of versions, along with a characterization of how the versions are related, and properties known to be true of each version. The versions are given in different notations connected through a core notation by compilers from and to the notations of existing tools and specification methods. The reasons that translations cannot always be exact are analyzed. To facilitate optimizations during retranslation, error tracing, and analysis, additional information is gathered during translation, and is also included with the system being analyzed.

The concept of a faithful relation among models and families of properties true of those models is presented. In this framework families of properties are provided with uniform syntactic transformations, in addition to the translations of the models. This framework generalizes common instances of relations among translations previously treated in an ad hoc way. The example of refinement translations is shown in detail. The classes of properties that can be faithful for a given translation provide a measure of the usefulness of the translation.