, A relational approach to defining and implementing transformations between metamodels, Journal of Software and Systems Modeling ( SoSyM), pp.215-239, 2003.
DOI : 10.1007/s10270-003-0032-z
, Towards The Formal Verification of Model Transformations ? An Application to Kermeta, 2013.
, Towards a model transformation intent catalog, Proceedings of the First Workshop on the Analysis of Model Transformations, AMT '12, 2012.
DOI : 10.1145/2432497.2432499
, A Tridimensional Approach for Studying the Formal Verification of Model Transformations, 2012 IEEE Fifth International Conference on Software Testing, Verification and Validation, 2012.
DOI : 10.1109/ICST.2012.197
URL : https://hal.archives-ouvertes.fr/hal-00684717
, Analysis of Model Transformations via Alloy, MoDeVVa, pp.47-56, 2007.
, 15 Years of Triple Graph Grammars, International Conference on Graph Transformation ( Icgt), pp.411-425, 2008.
DOI : 10.1007/978-3-540-87405-8_28
, A Graphical Approach to Prove the Semantic Preservation of UML/OCL Refactoring Rules, 6th International Andrei Ershov Memorial Conference ? Perspectives of Systems Informatics Psi, pp.70-83, 2006.
DOI : 10.1007/978-3-540-70881-0_9
, An Extended MDA Architecture for Ensuring Semantics-Preserving Transformations, Annual Ieee Software Engineering Workshop ( Sew), 2008.
, DSLTrans: A Turing Incomplete Transformation Language, Software Language Engineering ( Sle), 2010.
DOI : 10.1007/978-3-642-19440-5_19
, Barriers to systematic model transformation testing, Communications of the ACM, vol.53, issue.6, pp.139-143, 2010.
DOI : 10.1145/1743546.1743583
URL : https://hal.archives-ouvertes.fr/inria-00542747
, Symbolic invariant verification for systems with dynamic structural adaptation, Proceeding of the 28th international conference on Software engineering , ICSE '06, 2006.
DOI : 10.1145/1134285.1134297
, Automatic Termination Proofs for Programs with Shape-Shifting Heaps, Computer- Aided Verification ( Cav), pp.386-400, 2006.
DOI : 10.1007/11817963_35
, Interactive Theorem Proving and Program Development ? Coq'Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00344237
, Object-Oriented Software Construction, 2000.
, Local Confluence Analysis of Consistent Emf Transformations Electronic Communications of the European Association of Software Science and Technology Easst, pp.68-84, 2011.
, Formal Verification of Java Code Generation From UML Models, Fujaba Days, 2005.
, The Jamda Website http
, MoMent: A Formal Framework for Model manageMent, 2007.
, Towards a Systematic Method for Proving Termination of Graph Transformation Systems, Electronic Notes in Theoretical Computer Science ( Entcs), vol.213, issue.1, pp.23-28, 2008.
, The Bidirectional Transformations (Bx) Community Wiki http
, Model Transformations? Transformation Models! In Model Driven Engineering Languages and Systems ( MoDELS), Lecture Notes in Computer Science, 2006.
, 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
, Verification of UML/OCL Class Diagrams Using Constraint Programming, International Workshop on Model-Driven Engineering, Verification, and Validation (MoDeVVa), pp.73-80, 2008.
URL : https://hal.archives-ouvertes.fr/hal-00974321
, A Type-Theoretic Framework for Certified Model Transformations, Formal Methods: Foundations and Applications, pp.112-127, 2011.
DOI : 10.1007/11663430_13
, Verification of Model Transformations, Electronic Notes in Theoretical Computer Science, vol.292, pp.5-25, 2013.
DOI : 10.1016/j.entcs.2013.02.002
, Alexandre Feugas, and Franck Barbier Contracts for Model Execution Verification, Ecmfa, volume 6698 of Lncs, pp.3-18, 2011.
, Franck Barbier, and Nidal Djemam. OCL Contracts For The Verification Of Model Transformations, Workshop on the Pragmatics of Ocl and Other Textual Specification Languages, 2009.
, A relationship-based approach to model integration, Innovations in Systems and Software Engineering, vol.11, issue.3, pp.3-18, 2011.
DOI : 10.1007/s11334-011-0155-2
, All About Maude. A High- Performance Logical Framework, Lecture Notes in Computer Science, vol.4350, 2007.
, Essay on Semantics Definition in MDE - An Instrumented Approach for Model Verification, Journal of Software, vol.4, issue.9, pp.943-958, 2009.
DOI : 10.4304/jsw.4.9.943-958
, Implementing Mathematics with The NuPrl Proof Development System, 1984.
, A Gentle Introduction to Formal Verification of Computer Systems by Abstract Interpretation, Javier Esparza, 2011.
URL : https://hal.archives-ouvertes.fr/inria-00543886
, Feature-based survey of model transformation approaches, IBM Systems Journal, vol.45, issue.3, pp.621-645, 2006.
DOI : 10.1147/sj.453.0621
, Bidirectional Transformations: A Cross-Discipline Perspective (Grace Meeting Notes, State of the Art, and Outlook), International Conference on Model Transformation: Theory And Practice ( Icmt), pp.260-283, 2008.
, Pattern-Based Model-to-Model Transformation, International Conference on Graph Transformations ( Icgt), pp.426-441, 2008.
, Using AToM 3 as a Meta-Case Tool, International Conference on Enterprise Information Systems ( Iceis), pp.642-649, 2002.
, Automating the Transformation-Based Analysis of Visual Languages, Formal Aspects of Computing, vol.22, issue.3-4, pp.297-326, 2010.
, Information Preserving Bidirectional Model Transformations, International Conference on Fundamental Approaches to Software Engineering ( Fase), pp.72-86, 2007.
DOI : 10.1007/978-3-540-71289-3_7
, Termination Criteria for Model Transformation, International Conference on Fundamental Approaches to Software Engineering ( Fase), 2005.
, Design Patterns: Elements of Reusable Object-Oriented Software, 1995.
, A Classification of Model Checking-Based Verification Approaches for Software Models, Proceedings of the Second Workshop on Verification And Validation of Model Transformations ( Volt), 2013.
, Combining Formal Methods and Mde Techniques for Model-Driven System Design and Analysis, Journal On Advances in Software, vol.3, issue.12, pp.1-18, 2010.
, Confluence of aspects for sequence diagrams, Software & Systems Modeling, vol.16, issue.3, pp.789-824, 2011.
DOI : 10.1007/s10270-011-0212-1
, Pattern-Based Model-to-Model Transformation: Handling Attribute Conditions, Proceedings of the 2nd International Conference on Theory and Practice of Model Transformations ( Icmt), pp.83-99, 2009.
DOI : 10.5381/jot.2008.7.3.a3
, Automated verification of model transformations based on visual contracts, Automated Software Engineering, vol.32, issue.8, pp.5-46, 2013.
DOI : 10.1007/s10515-012-0102-y
, Facilités de Typage pour l'Ingénierie des Modèles, p.2013
, On Model Subtyping, 8th European Conference on Modelling Foundations and Applications ( Ecmfa), pp.400-415, 2012.
DOI : 10.1007/978-3-642-31491-9_30
URL : https://hal.archives-ouvertes.fr/hal-00726399
, On the Formal Verification of Systems of Synchronous Software Components, Computer Safety, Reliability, and Security, pp.291-304, 2012.
DOI : 10.1007/978-3-642-33678-2_25
, Meaningful modeling: what's the semantics of "semantics"?, Computer, vol.37, issue.10, pp.64-72, 2004.
DOI : 10.1109/MC.2004.172
, Confluence of Typed Attributed Graph Transformation Systems, International Conference on Graph Transformation ( Icgt), 2002.
DOI : 10.1007/3-540-45832-8_14
, Model synchronization based on triple graph grammars: correctness, completeness and invertibility, Journal of Software and Systems Modeling ( SoSyM), pp.1-29, 2013.
DOI : 10.1007/s10270-012-0309-1
, A Survey of Triple Graph Grammar Tools, International Workshop on Bidirectional Transformations ( Bx), 2013.
, Towards Verified Model Transformations, International Workshop on Model-Driven Engineering, Verification, and Validation ( MoDeVVa), pp.78-93, 2006.
, Software Abstractions: Logic, Language and Analysis, 2011.
, An Analysis and Survey of the Development of Mutation Testing, IEEE Transactions on Software Engineering, vol.37, issue.5, pp.649-678, 2010.
DOI : 10.1109/TSE.2010.62
, Aspect Categories and Classes of Temporal Properties. Transactions on Aspect-Oriented Software Development, pp.106-134, 2006.
, Domain-Specific Modeling: Enabling Full Code Generation, 2008.
DOI : 10.1002/9780470249260
, Guidelines for performing Systematic Literature Reviews in Software Engineering, 2007.
, Procedures for Undertaking Systematic Reviews, 2004.
, The Epsilon Book. The Eclipse Foundation, 2012.
, Tool Integration with Triple Graph Grammars ? A Survey, Electronic Notes in Theoretical Computer Science ( Entcs), vol.148, issue.1, pp.113-150, 2006.
, Systematic Transformation Development, Electronic Communications of the European Association of Software Science and Technology Easst, 2009.
, Definition and Validation of Model Transformations, Journal of Software and Systems Modeling ( SoSyM), vol.5, issue.3, pp.233-259, 2006.
, Efficient Detection of Conflicts in Graph-based Model Transformation, Electronic Notes in Theoretical Computer Science, vol.152, pp.97-109, 2006.
DOI : 10.1016/j.entcs.2006.01.017
, Specification and Verification of Model Transformations Using UML-RSDS, Integrated Formal Methods (i Fm), pp.199-214, 2010.
DOI : 10.1016/j.infsof.2007.04.003
URL : https://hal.archives-ouvertes.fr/inria-00525175
, Proving Model Transformations, 2010 4th IEEE International Symposium on Theoretical Aspects of Software Engineering, pp.35-44, 2010.
DOI : 10.1109/TASE.2010.16
, Supporting domain-specific model patterns with metamodeling, Software & Systems Modeling, vol.2, issue.3, pp.501-520, 2009.
DOI : 10.1007/s10270-009-0118-3
, A Technique for Automatic Validation of Model Transformations, International Conference on Model Driven Engineering Languages and Systems ( MoDELS), 2010.
DOI : 10.1007/978-3-642-16145-2_10
, Model transformation intents and their properties, Software & Systems Modeling, vol.211, issue.1, pp.1-38, 2013.
DOI : 10.1007/s10270-014-0429-x
, Coupled Software Transformations (Extended Abstract), First International Workshop on Software Evolution Transformations, pp.31-35, 2004.
, Towards Automated, Formal Verification of Model Transformations, 2010 Third International Conference on Software Testing, Verification and Validation, 2010.
DOI : 10.1109/ICST.2010.42
, Refactoring OCL annotated UML class diagrams, Software & Systems Modeling, vol.20, issue.5, pp.25-47, 2008.
DOI : 10.1007/s10270-007-0056-x
, Formal Refactoring for UML Class Diagrams, 17th Brazilian Symposium on Software Engineering ( Sbse), pp.152-167, 2005.
, A Taxonomy of Model Transformation, Electronic Notes in Theoretical Computer Science, vol.152, pp.125-142, 2006.
DOI : 10.1016/j.entcs.2005.10.021
, A Platform for Experimenting with Language Constructs for Modularizing Crosscutting Concerns, Proceedings of the Third International Workshop on Academic Software Development Tools and Techniques ( WASDeTT), 2010.
, Weaving Executability into Object-Oriented Meta-languages, Proceedings of the 8th international conference on Model Driven Engineering Languages and Systems ( MoDels), pp.264-278, 2005.
DOI : 10.1007/11557432_19
URL : https://hal.archives-ouvertes.fr/hal-00795095
, Specifying the correctness properties of model transformations, Proceedings of the third international workshop on Graph and model transformations, GRaMoT '08, pp.45-52, 2008.
DOI : 10.1145/1402947.1402957
, Towards Verifying Model Transformations, Electronic Notes in Theoretical Computer Science, vol.211, pp.191-200, 2008.
DOI : 10.1016/j.entcs.2008.04.041
, Verifying Model Transformation By Structural Correspondence Electronic Communications of the European Association of Software Science and Technology Easst, pp.15-29, 2008.
, On Theories With a Combinatorial Definition, Annals of Mathematics, vol.43, issue.2, pp.223-243, 1942.
, Using Fujaba for the Development of Production Control Systems, Proceedings of the International Workshop and Symposium on Applications Of Graph Transformations With Industrial Relevance ( Agtive), pp.191-191, 1999.
DOI : 10.1007/3-540-45104-8_13
, Isabelle/ Hol: A Proof Assistant for Higher-Order Logic, volume 2283 of Lecture Notes in Computer Science, 2013.
DOI : 10.1007/3-540-45949-9
, On the Specification and Verification of Model Transformations, Semantics and Algebraic Specification, pp.140-161, 2009.
DOI : 10.1007/3-540-59071-4_45
, Refinement versus Verification: Compatibility of Net Invariants and Stepwise Development of High-Level Petri Nets, 1997.
, Metamodel- Based Model Conformance and Multi-View Consistency Checking, Acm Transactions on Software Engineering and Methodology ( Tosem), vol.16, issue.3, pp.1-48, 2007.
, Two Basic Correctness Properties for Atl Transformations: Executability and Coverage, Third International Workshop on Model Transformation with ATL ( Mt-Atl), 2008.
URL : https://hal.archives-ouvertes.fr/inria-00610205
, Termination of Graph Rewriting is Undecidable, Fundamenta Informaticae, vol.33, issue.2, pp.201-209, 1998.
, Confluence of Graph Transformation Revisited, Processes, Terms and Cycles: Steps on the Road to Infinity, 2005.
DOI : 10.1007/11601548_16
, The Meta-Object Facility (Mof) Typed, Acm Symposium on Applied computing ( Sac), pp.1845-1849, 2006.
, Proofs-as-Model-Transformations, Theory and Practice of Model Transformations, pp.214-228, 2008.
DOI : 10.1007/978-3-540-69927-9_15
, Verifying Semantic Conformance of State Machine-to-Java Code Generators, Proceedings of the International Conference on Model Driven Engineering Languages and Systems ( MoDELS), pp.166-180, 2010.
, A Survey of Approaches for Verifying Model Transformations, Journal of Software and Systems ( SoSyM), pp.1-26, 2013.
, Behavior Preservation in Model Refactoring Using DPO Transformations with Borrowed Contexts, Proceedings of the International Conference on Graph Transformations ( Icmt), pp.242-256, 2008.
DOI : 10.1007/978-3-540-87405-8_17
, Behavioral Refinement of Graph Transformation-Based Models, Electronic Notes in Theoretical Computer Science, vol.127, issue.3, pp.101-111, 2005.
DOI : 10.1016/j.entcs.2004.08.037
, Model Checking Graph Transformations: A Comparison of Two Approaches, International Conference on Graph Transformation ( Icgt), 2004.
DOI : 10.1007/978-3-540-30203-2_17
, Formal Specification and Analysis of Domain-Specific Models Using Maude, Simulation, vol.85, pp.11-12778, 2009.
, On The Semantics of Real-Time Domain-Specific Modeling of Languages, 2010.
, Analyzing Rule-Based Behavioral Semantics of Visual Modeling Languages with Maude, Proceeding of the International Conference on Software Language Engineering ( Sle), pp.54-73, 2009.
DOI : 10.1007/978-3-540-73859-6_12
, Verification of Model Transformations, Proceedings of the Ninth International Workshop on Graph Transformation and Visual Modeling Techniques, 2010.
, Model Transformation Testing: The State of the Art, Analysis of Model Transformations, p.2012
, Model transformation: the heart and soul of model-driven software development, IEEE Software, vol.20, issue.5, pp.42-45, 2003.
DOI : 10.1109/MS.2003.1231150
, Path-Length Analysis of Object-Oriented Programs, International Workshop on Emerging Applications of Abstract Interpretation ( Eaai), 2006.
, On model typing, Software & Systems Modeling, vol.3, issue.5, pp.401-413, 2007.
DOI : 10.1007/s10270-006-0036-6
URL : https://hal.archives-ouvertes.fr/inria-00477547
, Formal Verification of QVT Transformations for Code Generation, International Conference on Model Driven Engineering Languages and Systems ( MoDELS), 2011.
, A Landscape of Bidirectional Model Transformations, Summer School on Generative and Transformational Techniques in Software Engineering, pp.408-424, 2008.
DOI : 10.1007/978-3-540-88643-3_10
, Bidirectional Model Transformations in Qvt: Semantic Issues and Open Questions, Journal of Software and Systems, vol.9, issue.1, pp.7-20, 2009.
, A Multi-Paradigm Foundation for Model Transformation Language Engineering, 2011.
, AGG: A Tool Environment for Algebraic Graph Transformation, Proceedings of the International Workshop and Symposium on Applications Of Graph Transformations With Industrial Relevance ( Agtive), pp.333-341, 2000.
DOI : 10.1007/3-540-45104-8_41
, 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
, Automated Formal Verification of Model Transformations, Proceedings of the Critical Systems Development in UML Workshop, pp.63-78, 2003.
, Termination Analysis of Model Transformations by Petri Nets, International Conference on Graph Transformation ( Icgt), pp.260-274, 2006.
DOI : 10.1007/11841883_19
, A Static Analyzer for Model Transformations, Third International Workshop on Model Transformations with Atl, 2011.
, Right or Wrong? Verification, Journal of Object Technology, vol.V, issue.N, 2011.
, The Formal Semantics of Programming Languages: An Introduction (Foundations of Computing), 1993.
, Testing, abstraction, theorem proving, Proceedings of the 2006 international symposium on Software testing and analysis , ISSTA'06, pp.145-156, 2006.
DOI : 10.1145/1146238.1146255
, Contact: Benoit.Combemale@irisa.fr, or visit http
, Selim received a M.Sc. from Cairo University (Faculty of Computers and Information) in Egypt and is currently a Ph.D. candidate in the School of Computing of Queen's University in Canada. Her research interests include model transformations, model transformation intents, testing of model transformations, formal verification of model transformations, and software product lines
, Institut National Polytechnique He is currently Professeur at the University of Luxembourg, working on the topics of software testing, model-driven engineering, model based testing, evolutionary algorithms , software security, security policies and Android security, and exploring key topics related to Internet of things (IoT), Big Data (stress testing, multi-objective optimization and data protection), and mobile security and reliability. He is also the current head of the Csc Research Unit of the University, and member of the Interdisciplinary Centre for Security, Reliability and Trust (SnT), leading the Serval (SEcurity Reasoning and VALidation) Research Group. He (co-)authored more than 140 publications in international peer-reviewed conferences and journals. Contact: Yves.LeTraon@uni.lu, or visit https, 1997.
, As leader of the Txl source transformation project with hundreds of academic and industrial users worldwide, he is the author of more than 160 refereed contributions in programming languages, software engineering and artificial intelligence. Dr. Cordy is an Acm Distinguished Scientist, a senior member of the Ieee and an Ibm Cas faculty fellow, Contact: Cordy@cs.queensu.ca