A. W. Appel, L. Beringer, A. Chlipala, B. C. Pierce, Z. Shao et al., Position paper: the science of deep specification, Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences, vol.375, p.2104, 2017.

. Atlas-group, Specification of the ATL Virtual Machine, 2005.

B. Baudry, S. Ghosh, F. Fleurey, R. France, Y. L. Traon et al., Barriers to systematic model transformation testing, Commun. ACM, vol.53, pp.139-143, 2010.
URL : https://hal.archives-ouvertes.fr/inria-00542747

V. Benzaken and E. Contejean, A Coq mechanised formal semantics for realistic SQL queries: formally reconciling SQL and bag relational algebra, 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp.249-261, 2019.
URL : https://hal.archives-ouvertes.fr/hal-01955433

V. Benzaken, E. Contejean, C. Keller, and E. Martins, A Coq Formalisation of SQL's Execution Engines, 9th International Conference on Interactive Theorem Proving, pp.88-107, 2018.

G. Berry, Synchronous Design and Verification of Critical Embedded Systems Using SCADE and Esterel, 12th International Workshop on Formal Methods for Industrial Critical Systems, 2008.

M. Bodin, A. Chargueraud, D. Filaretti, P. Gardner, S. Maffeis et al., A Trusted Mechanised JavaScript Specification, 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp.87-100, 2014.
URL : https://hal.archives-ouvertes.fr/hal-00910135

F. Büttner, M. Egea, and J. Cabot, On verifying ATL transformations using 'off-the-shelf' 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.

D. Calegari, C. Luna, N. Szasz, and Á. Tasistro, A Type-Theoretic Framework for Certified Model Transformations, 13th Brazilian Symposium on Formal Methods, pp.112-127, 2011.

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.

Z. Cheng and M. Tisi, A Deductive Approach for Fault Localization in ATL Model Transformations, 20th International Conference on Fundamental Approaches to Software Engineering, pp.300-317, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01435977

Z. Cheng and M. Tisi, Incremental Deductive Verification for Relational Model Transformations, 10th IEEE International Conference on Software Testing, Verification and Validation, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01435974

Z. Cheng and M. Tisi, Slicing ATL model transformations for scalable deductive verification and fault localization, International Journal on Software Tools for Technology Transfer, vol.20, pp.645-663, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01763410

Z. Cheng, M. Tisi, and R. Douence, CoqTL: a Coq DSL for rule-based model transformation, Software & Systems Modeling, vol.19, pp.425-439, 2020.
URL : https://hal.archives-ouvertes.fr/hal-02333564

A. Chlipala, B. Delaware, S. Duchovni, J. Gross, C. Pit-claudel et al., The End of History? Using a Proof Assistant to Replace Language Design with Library Design, 2nd Summit on Advances in Programming Languages, pp.1-15, 2017.

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. EPTCS, pp.63-77, 2013.

X. He and Z. Hu, Putback-based bidirectional model transformations, 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, pp.434-444, 2018.

S. Hidaka, F. Jouault, and M. Tisi, On Additivity in Transformation Languages, 20th International Conference on Model Driven Engineering Languages and Systems, pp.23-33, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01566259

F. Jouault, F. Allilaire, J. Bézivin, and I. Kurtev, ATL: A Model Transformation Tool, Science of Computer Programming, vol.72, pp.31-39, 2008.

F. Jouault and J. Bézivin, KM3: A DSL for Metamodel Specification, 8th International Conference on Formal Methods for Open Object-Based Distributed Systems, pp.171-185, 2006.
URL : https://hal.archives-ouvertes.fr/hal-00448119

R. F. Dimitrios-s-kolovos, F. Paige, and . Polack, The Epsilon transformation language, 1st International Conference on Model Transformations, 2008.

. Springer, , pp.46-60

K. Lano, T. Clark, and S. Kolahdouz-rahimi, A framework for model transformation verification, Formal Aspects of Computing, vol.27, pp.193-235, 2014.

X. Leroy, Formal Verification of a Realistic Compiler, Commun. ACM, vol.52, pp.107-115, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00415861

S. Martínez, M. Tisi, and R. Douence, Reactive model transformation with ATL, Science of Computer Programming, vol.136, pp.1-16, 2017.

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

, Query/View/Transformation Specification, 2016.

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.

T. Ringer, N. Yazdani, J. Leo, and D. Grossman, Adapting proof automation to adapt proofs, 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp.115-129, 2018.

G. Ro?u and . Traian-florin-?erb?nu??, An Overview of the K Semantic Framework, Journal of Logic and Algebraic Programming, vol.79, pp.397-434, 2010.

.. K. Gehanm, S. Selim, J. Wang, J. Cordy, and . Dingel, Model Transformations for Migrating Legacy Models: An Industrial Case Study, 8th European Conference on Modelling Foundations and Applications, pp.90-101, 2012.

K. Stenzel, N. Moebius, and W. Reif, Formal verification of QVT transformations for code generation, Software & Systems Modeling, vol.14, pp.981-1002, 2015.

M. Tisi and Z. Cheng, CoqTL: An internal DSL for model transformation in Coq, 11th International Conference on Model Transformations, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01828344

S. Springer, , pp.142-156

M. Tisi, S. Martínez, F. Jouault, and J. Cabot, Lazy execution of model-to-model transformations, 14th International Conference on Model Driven Engineering Languages and Systems, pp.32-46, 2011.
URL : https://hal.archives-ouvertes.fr/inria-00609458

J. Troya and A. Vallecillo, A Rewriting Logic Semantics for ATL, Journal of Object Technology, vol.10, pp.1-29, 2011.

G. Varró, K. Friedl, and D. Varró, Implementing a graph transformation engine in relational databases, Software & Systems Modeling, vol.5, issue.3, pp.313-341, 2006.

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

D. Wagelaar, M. Tisi, J. Cabot, and F. Jouault, Towards a General Composition Semantics for Rule-Based Model Transformation, 14th International Conference on Model Driven Engineering Languages and Systems, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00642066

. Springer, , pp.623-637