. Ab, L. Rahim, and J. Whittle, A survey of approaches for verifying model transformations, Software & Systems Modeling, vol.14, issue.2, pp.1003-1028, 2015.

G. Berry, Synchronous Design and Verification of Critical Embedded Systems Using SCADE and Esterel, 12th International Workshop on Formal Methods for Industrial Critical Systems, pp.2-2, 2008.
DOI : 10.1007/978-3-540-79707-4_2

F. Büttner, M. Egea, and J. Cabot, On verifying ATL transformations using 'off-theshelf' SMT solvers, 15th International Conference on Model Driven Engineering Languages and Systems, pp.198-213, 2012.

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, pp.198-213, 2012.
DOI : 10.1007/978-3-642-34281-3_16

D. Calegari, C. Luna, N. Szasz, and ´. A. Tasistro, A Type-Theoretic Framework for Certified Model Transformations, 13th Brazilian Symposium on Formal Methods, pp.112-127, 2011.
DOI : 10.1007/11663430_13

Z. Cheng, R. Monahan, and J. F. Power, A Sound Execution Semantics for ATL via Translation Validation, 8th International Conference on Model Transformation, pp.133-148, 2015.
DOI : 10.1007/978-3-319-21155-8_11
URL : http://eprints.maynoothuniversity.ie/8221/1/JP-Sound-2015.pdf

A. Chlipala, The Bedrock structured programming system: Combining generative metaprogramming and hoare logic in an extensible program verifier, 18th ACM SIGPLAN International Conference on Functional Programming. pp. 391? 402. ICFP '13, 2013.
DOI : 10.1145/2544174.2500592

J. S. Cuadrado, J. G. Molina, and M. M. Tortosa, RubyTL: A Practical, Extensible Transformation Language, 2nd European Conference on Model Driven Architecture: Foundations and Applications, pp.158-172, 2006.
DOI : 10.1007/11787044_13
URL : http://www.modelum.es/papers/ecmda2006.rubytl.jsanchez.pdf

M. Fernández and J. Terrell, Assembling the Proofs of Ordered Model Transformations, 10th International Workshop on Formal Engineering approaches to Software Components and Architectures, pp.63-77, 2013.
DOI : 10.1007/978-3-642-16901-4_6

R. Gu, Z. Shao, H. Chen, X. Wu, J. Kim et al., CertiKOS, Proceedings of the Second Asia-Pacific Workshop on Systems, APSys '11, pp.653-669, 2016.
DOI : 10.1145/2103799.2103803

M. K. Hamiaz, M. Pantel, B. Combemale, and X. Thirioux, A formal framework to prove the correctness of model driven engineering composition operators, International Conference on Formal Engineering Methods, 2014.

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

D. S. Kolovos, R. F. Paige, and F. A. Polack, The Epsilon Transformation Language, 1st International Conference on Model Transformations, pp.46-60, 2008.
DOI : 10.1007/978-3-540-69927-9_4

K. Lano, T. Clark, and S. Kolahdouz-rahimi, A framework for model transformation verification, Formal Aspects of Computing, vol.88, issue.2, pp.193-235, 2014.
DOI : 10.1007/978-3-540-69927-9_15
URL : http://shura.shu.ac.uk/12046/1/mtsem.pdf

X. Leroy, Formal certification of a compiler back-end or, ACM SIGPLAN Notices, vol.41, issue.1, pp.42-54, 2006.
DOI : 10.1145/1111320.1111042
URL : https://hal.archives-ouvertes.fr/inria-00000963

B. J. Oakes, J. Troya, L. Lúcio, and M. Wimmer, Fully verifying transformation contracts for declarative ATL, 2015 ACM/IEEE 18th International Conference on Model Driven Engineering Languages and Systems (MODELS), pp.256-265, 2015.
DOI : 10.1109/MODELS.2015.7338256

C. Picard and R. Matthes, Coinductive graph representation: the problem of embedded lists, Electronic Communications of the EASST, vol.39, 2011.
DOI : 10.1007/978-3-642-32784-1_12
URL : https://hal.inria.fr/hal-01539884/file/978-3-642-32784-1_12_Chapter.pdf

B. C. Pierce, A. A. De-amorim, C. Casinghino, M. Gaboardi, M. Greenberg et al., Software Foundations. Electronic textbook, 2017.

I. Poernomo and J. Terrell, Correct-by-Construction Model Transformations from Partially Ordered Specifications in Coq, 12th International Conference on Formal Engineering Methods, pp.56-73, 2010.
DOI : 10.1007/978-3-540-69927-9_15

G. Selim, S. Wang, J. Cordy, and J. Dingel, Model Transformations for Migrating Legacy Models: An Industrial Case Study, 8th European Conference on Modelling Foundations and Applications, pp.90-101, 2012.
DOI : 10.1007/978-3-642-31491-9_9

K. Stenzel, N. Moebius, and W. Reif, Formal verification of QVT transformations for code generation, Software & Systems Modeling, vol.14, p.9811002, 2015.
DOI : 10.1007/s10270-013-0351-7

D. Wagelaar, Using ATL/EMFTVM for import/export of medical data, 2nd Software Development Automation Conference, 2014.

Z. Yang, K. Hu, D. Ma, J. P. Bodeveix, L. Pi et al., From AADL to Timed Abstract State Machines: A verified model transformation, Journal of Systems and Software, vol.93, pp.42-68, 2014.
DOI : 10.1016/j.jss.2014.02.058
URL : https://hal.archives-ouvertes.fr/hal-01123837