Abstract
Abstract
While verifying the correctness of model transformations is becoming increasingly important, current model transformation languages offer only weak support for checking statically that transformations can not go wrong. This paper presents conditions under which transformations can be shown to produce models that conform to their meta-models, and it describes methods to derive prove obligations from a set of transformation rules.