. 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.

J. R. Abrial, M. Butler, S. Hallerstede, T. S. Hoang, F. Mehta et al., Rodin: an open toolset for modelling and reasoning in Event-B, International Journal on Software Tools for Technology Transfer, vol.15, issue.1, pp.447-466, 2010.
DOI : 10.1007/978-3-642-18216-7

V. Aranega, J. Mottu, A. Etien, and J. Dekeyser, Traceability mechanism for error localization in model transformation, 4th International Conference on Software and Data Technologies, pp.66-73, 2009.
URL : https://hal.archives-ouvertes.fr/hal-00461266

M. Barnett, B. Y. Chang, R. Deline, B. Jacobs, and K. R. Leino, Boogie: A Modular Reusable Verifier for Object-Oriented Programs, 4th International Conference on Formal Methods for Components and Objects, pp.364-387, 2006.
DOI : 10.1007/11804192_17

S. Berghofer and T. Nipkow, Random testing in Isabelle/HOL, Proceedings of the Second International Conference on Software Engineering and Formal Methods, 2004. SEFM 2004., pp.230-239, 2004.
DOI : 10.1109/SEFM.2004.1347524

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

Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development: Coq'Art The Calculus of Inductive Constructions, 2010.
DOI : 10.1007/978-3-662-07964-5
URL : https://hal.archives-ouvertes.fr/hal-00344237

L. C. Briand, Making model-driven verification practical and scalable -experiences and lessons learned, 4th International Conference on Model-Driven Engineering and Software Development. SCITEPRESS, 2016.

L. Burgueño, J. Troya, M. Wimmer, and A. Vallecillo, Static Fault Localization in Model Transformations, IEEE Transactions on Software Engineering, vol.41, issue.5, pp.490-506, 2015.
DOI : 10.1109/TSE.2014.2375201

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.
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, 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
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

Z. Cheng, R. Monahan, and J. F. Power, Formalised EMFTVM bytecode language for sound verification of model transformations. Software & Systems Modeling p, 2016.

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.
DOI : 10.1007/978-3-642-41533-3_40
URL : https://hal.archives-ouvertes.fr/hal-01435977

K. Claessen and J. Hughes, QuickCheck, ACM SIGPLAN Notices, vol.46, issue.4, pp.53-64, 2011.
DOI : 10.1145/1988042.1988046

J. S. Cuadrado, E. Guerra, and J. De-lara, Uncovering Errors in ATL Model Transformations Using Static Analysis and Constraint Solving, 2014 IEEE 25th International Symposium on Software Reliability Engineering, pp.34-44, 2014.
DOI : 10.1109/ISSRE.2014.10

J. S. Cuadrado, E. Guerra, J. De-lara, R. Clarisó, and J. Cabot, Translating Target to Source Constraints in Model-to-Model Transformations, 2017 ACM/IEEE 20th International Conference on Model Driven Engineering Languages and Systems (MODELS), pp.12-22, 2017.
DOI : 10.1109/MODELS.2017.12

J. C. Filliâtre and A. Paskevich, Why3 ??? Where Programs Meet Provers, 22nd European Symposium on Programming, pp.125-128
DOI : 10.1007/978-3-642-37036-6_8

M. Harman, D. Binkley, and S. Danicic, Amorphous program slicing, Journal of Systems and Software, vol.68, issue.1, pp.45-64, 2003.
DOI : 10.1016/S0164-1212(02)00135-8
URL : http://www.brunel.ac.uk/~csstmmh2/jss1.ps

J. Hatcliff, G. T. Leavens, K. R. Leino, P. Müller, and M. J. Parkinson, Behavioral interface specification languages, ACM Computing Surveys, vol.44, issue.3, pp.1-1658, 2012.
DOI : 10.1145/2187671.2187678

S. Hidaka, F. Jouault, and M. Tisi, On Additivity in Transformation Languages, 2017 ACM/IEEE 20th International Conference on Model Driven Engineering Languages and Systems (MODELS), pp.2017-2040, 2017.
DOI : 10.1109/MODELS.2017.21
URL : https://hal.archives-ouvertes.fr/hal-01566259

C. A. Hoare, An axiomatic basis for computer programming, Communications of the ACM, vol.12, issue.10, pp.576-580, 1969.
DOI : 10.1145/363235.363259
URL : http://www.utdallas.edu/~kxh060100/cs6371fa07/hoare.pdf

W. A. Howard, The formulae-as-types notion of construction, To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp.479-490, 1980.

M. Huth and M. Ryan, Logic in Computer Science: Modelling and Reasoning About Systems, 2004.
DOI : 10.1017/CBO9780511810275

Y. Jia and M. Harman, An Analysis and Survey of the Development of Mutation Testing, IEEE Transactions on Software Engineering, vol.37, issue.5, pp.649-678, 2011.
DOI : 10.1109/TSE.2010.62

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

T. Kehrer, G. Taentzer, M. Rindt, and U. Kelter, Automatically Deriving the Specification of Model Editing Operations from Meta-Models, 9th International Conference on Model Transformation, pp.173-188, 2016.
DOI : 10.1016/j.scico.2012.06.002

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

K. R. Leino, M. Moskal, and W. Schulte, Verification condition split- ting. https://www.microsoft. com/en-us, 2008.

L. De-moura and N. Bjørner, Z3: An Efficient SMT Solver, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp.337-340, 2008.
DOI : 10.1007/978-3-540-78800-3_24

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

M. Object and . Group, Unified modeling language (ver. 2.5) http://www.omg.org/ spec, 2015.

I. Poernomo, Proofs-as-Model-Transformations, 1st International Conference on Model Transformation. pp
DOI : 10.1007/978-3-540-69927-9_15

Z. Springer, S. Prasad, M. R. Biere, A. Gupta, and A. , A survey of recent advances in SAT-based formal verification, International Journal on Software Tools for Technology Transfer, vol.7, issue.2, pp.156-173, 2005.

H. Radke, T. Arendt, J. S. Becker, A. Habel, and G. Taentzer, Translating Essential OCL Invariants to Nested Graph Constraints Focusing on Set Operations, 8th International Conference on Graph Transformation, pp.155-170, 2015.
DOI : 10.1007/978-3-319-21145-9_10

A. Roychoudhury and S. Chandra, Formulabased software debugging, Communications of the ACM pp, pp.68-77, 2016.

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

D. Steinberg, F. Budinsky, E. Merks, and M. Paternostro, EMF: Eclipse modeling framework, 2008.

F. Tip, A survey of program slicing techniques, 1994.

M. Tisi, S. M. Perez, and H. Choura, Parallel Execution of ATL Transformation Rules, 16th International Conference on Model-Driven Engineering Languages and Systems, pp.656-672, 2013.
DOI : 10.1007/978-3-642-41533-3_40
URL : https://hal.archives-ouvertes.fr/hal-00869269

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

M. Weiser, Program Slicing, 5th International Conference on Software Engineering, pp.439-449, 1981.
DOI : 10.1109/TSE.1984.5010248

W. E. Wong, R. Gao, Y. Li, R. Abreu, and F. Wotawa, A Survey on Software Fault Localization, IEEE Transactions on Software Engineering, vol.42, issue.8, pp.1-41, 2016.
DOI : 10.1109/TSE.2016.2521368