K. Anastasakis, B. Bordbar, and J. M. Küster, Analysis of Model Transformations via Alloy, MoDeVVa'2007, Proceedings, 2007.

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

G. Atl-user, Website, eclipse.org/ATL, 2012.

L. Baresi and P. Spoletini, On the Use of Alloy to Analyze Graph Transformation Systems, Third International Conference on Graph Transformations, ICGT 2006. Proceedings., volume 4178 of LNCS, pp.306-320, 2006.
DOI : 10.1007/11841883_22

B. Baudry, S. Ghosh, F. Fleurey, R. B. France, Y. L. Traon et al., Barriers to systematic model transformation testing, Communications of the ACM, vol.53, issue.6, 2010.
DOI : 10.1145/1743546.1743583
URL : https://hal.archives-ouvertes.fr/inria-00542747

B. Becker, L. Lambers, J. Dyck, S. Birth, and H. Giese, Iterative development of consistencypreserving rule-based refactorings, Theory and Practice of Model Transformations -4th International Conference, ICMT 2011 Proceedings, pp.123-137, 2011.

A. Boronat, R. Heckel, and J. Meseguer, Rewriting Logic Semantics and Verification of Model Transformations, FASE'09, Proceedings, 2009.
DOI : 10.1007/978-3-642-00593-0_2

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

F. Büttner, M. Egea, J. Cabot, and M. Gogolla, Verification of ATL Transformations Using Transformation Models and Model Finders, 14th International Conference on Formal Engineering Methods, ICFEM 2012 Proceedings, Lecture Notes in Computer Science, 2012.
DOI : 10.1007/978-3-642-34281-3_16

J. Cabot, R. Clariso, E. Guerra, and J. Lara, Verification and validation of declarative modelto-model transformations through invariants, Journal of Systems and Software, vol.83, issue.2, p.2010

M. Clavel, M. Egea, and M. A. De-dios, Checking unsatisfiability for OCL constraints, Electronic Communications of the EASST, vol.24, 2009.

L. M. De-moura and N. Bjørner, Satisfiability modulo theories, Communications of the ACM, vol.54, issue.9, pp.69-77, 2011.
DOI : 10.1145/1995376.1995394
URL : https://hal.archives-ouvertes.fr/hal-01095009

B. Dutertre and L. D. Moura, The Yices SMT solver, 2006.

H. Ehrig, K. Ehrig, U. Prange, and G. Taentzer, Fundamentals of Algebraic Graph Transformation (Monographs in Theoretical Computer Science. An EATCS Series), 2006.

Y. Ge and L. M. De-moura, Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories, Computer Aided Verification, CAV 2009, Proceedings, pp.306-320, 2009.
DOI : 10.1007/978-3-642-02658-4_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, 2008.
DOI : 10.1016/j.scico.2007.08.002
URL : https://hal.archives-ouvertes.fr/hal-00483363

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

K. Lano and S. K. Rahimi, Model-Driven Development of Model Transformations, Theory and Practice of Model Transformations -4th International Conference, ICMT 2011, pp.47-61, 2011.
DOI : 10.1007/978-3-642-21732-6_4

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

C. M. Poskitt and D. Plump, Hoare-style verification of graph programs, Fundamenta Informaticae, vol.118, issue.12, pp.135-175, 2012.

A. Rensink, Explicit State Model Checking for Graph Grammars, Concurrency, Graphs and Models, Essays Dedicated to Ugo Montanari on the Occasion of His 65th Birthday, pp.114-132, 2008.
DOI : 10.1007/978-3-540-68679-8_8
URL : http://doc.utwente.nl/62357/1/ugo2008.pdf

M. Richters and M. Gogolla, On Formalizing the UML Object Constraint Language OCL, Conceptual Modeling -ER '98, 17th International Conference on Conceptual Modeling Proceedings, volume 1507 of LNCS, pp.449-464, 1998.
DOI : 10.1007/978-3-540-49524-6_35

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