K. Anastasakis, B. Bordbar, G. Georg, and I. Ray, UML2Alloy: A Challenging Model Transformation, MoDELS 2007, 2007.
DOI : 10.1007/978-3-540-75209-7_30
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.101.7905

M. Asztalos, L. Lengyel, and T. Levendovszky, Towards Automated, Formal Verification of Model Transformations, 2010 Third International Conference on Software Testing, Verification and Validation, pp.15-24, 2010.
DOI : 10.1109/ICST.2010.42

C. Braga, R. Menezes, T. Comicio, C. Santos, and E. Landim, On the Specification, Verification and Implementation of Model Transformations with Transformation Contracts, SBMF 2011, 2011.
DOI : 10.1007/3-540-59071-4_45

F. Büttner, J. Cabot, and M. Gogolla, On validation of ATL transformation rules by transformation models, Proceedings of the 8th International Workshop on Model-Driven Engineering, Verification and Validation, MoDeVVa, 2011.
DOI : 10.1145/2095654.2095666

F. Büttner, M. Egea, and J. Cabot, On Verifying ATL Transformations Using ???off-the-shelf??? SMT Solvers, MoDELS'2012, to appear, 2012.
DOI : 10.1007/978-3-642-33666-9_28

J. Bézivin, F. Büttner, M. Gogolla, F. Jouault, I. Kurtev et al., Model Transformations? Transformation Models!, LNCS, vol.4199, 2006.
DOI : 10.1007/11880240_31

J. Cabot, R. Clarisó, E. Guerra, and J. De-lara, Verification and validation of declarative model-to-model transformations through invariants, Journal of Systems and Software, vol.83, issue.2, pp.283-302, 2010.
DOI : 10.1016/j.jss.2009.08.012
URL : https://hal.archives-ouvertes.fr/hal-00540816

J. Cabot, R. Clarisó, and D. Riera, UMLtoCSP, Proceedings of the twenty-second IEEE/ACM international conference on Automated software engineering , ASE '07, 2007.
DOI : 10.1145/1321631.1321737

E. Cariou, N. Belloir, F. Barbier, and N. Djemam, OCL contracts for the verification of model transformations, Electronic Communications of the EASST, vol.24, 2009.
URL : https://hal.archives-ouvertes.fr/hal-01093481

M. Clavel, M. Egea, and M. A. De-dios, Checking Unsatisfiability for OCL Constraints, Electronic Communications of the EASST, vol.24, pp.1-13, 2009.

M. Gogolla, Tales of ER and RE Syntax and Semantics, Transformation Techniques in Software Engineering. IBFI (2005), dagstuhl Seminar Proc. 05161

M. Gogolla and A. Vallecillo, Tractable Model Transformation Testing, ECMFA 2011, 2011.
DOI : 10.1007/978-3-642-21470-7_16
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.303.6300

E. Guerra, J. De-lara, D. S. Kolovos, and R. F. Paige, A Visual Specification Language for Model-to-Model Transformations, 2010 IEEE Symposium on Visual Languages and Human-Centric Computing, pp.119-126, 2010.
DOI : 10.1109/VLHCC.2010.25

K. Inaba, S. Hidaka, Z. Hu, H. Kato, and K. Nakano, Graph-transformation verification using monadic second-order logic, Proceedings of the 13th international ACM SIGPLAN symposium on Principles and practices of declarative programming, PPDP '11, pp.17-28, 2011.
DOI : 10.1145/2003476.2003482
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.675.28

F. Jouault, F. Allilaire, J. Bézivin, and I. Kurtev, ATL: A model transformation tool, Science of Computer Programming, vol.72, issue.1-2, pp.31-39, 2008.
DOI : 10.1016/j.scico.2007.08.002
URL : https://hal.archives-ouvertes.fr/hal-00483363

F. Jouault and J. Bézivin, KM3: A DSL for Metamodel Specification In: Formal Methods for Open Object-Based Distributed Systems, FMOODS 2006, Proc. LNCS, pp.171-185, 2006.

F. Jouault and I. Kurtev, Transforming Models with ATL, Proc. of the Model Transformations in Practice Workshop at MoDELS 2005, 2005.
DOI : 10.1007/11663430_14
URL : https://hal.archives-ouvertes.fr/hal-00448120

M. Kuhlmann, L. Hamann, and M. Gogolla, Extensive Validation of OCL Models by Integrating SAT Solving into USE, TOOLS 201, pp.290-306, 2011.
DOI : 10.1007/978-3-642-21952-8_21

L. Lucio, B. Barroca, and V. Amaral, A Technique for Automatic Validation of Model Transformations, MODELS 2010, Part I. LNCS, 2010.
DOI : 10.1007/978-3-642-16145-2_10

A. Rensink, Explicit State Model Checking for Graph Grammars, LNCS, vol.5065, pp.114-132, 2008.
DOI : 10.1007/978-3-540-68679-8_8

S. Sen, N. Moha, B. Baudry, and J. M. Jézéquel, Meta-model Pruning, MODELS 2009, Proc. LNCS, pp.32-46, 2009.
DOI : 10.1016/S1571-0661(04)80066-5
URL : https://hal.archives-ouvertes.fr/inria-00468514

M. Soeken, R. Wille, and R. Drechsler, Encoding OCL Data Types for SAT-Based Verification of UML/OCL Models, TAP 2011, pp.152-170, 2011.
DOI : 10.1016/S0747-7171(88)80004-X

D. Steinberg, F. Budinsky, M. Paternostro, and E. Merks, EMF: Eclipse Modeling Framework, 2008.

J. Troya and A. Vallecillo, A Rewriting Logic Semantics for ATL., The Journal of Object Technology, vol.10, issue.5, pp.1-29, 2011.
DOI : 10.5381/jot.2011.10.1.a5

J. B. Warmer and A. G. Kleppe, The Object Constraint Language: Getting Your Models Ready for MDA, 2003.