My research activities are conducted in the ACADIE team from the Institut de Recherche en Informatique de Toulouse (IRIT), UMR 5505 from the Centre National de la Recherche Scientifique (CNRS). I am part time member of the INGEQUIP team from Institut de Recherche Technologique (IRT) Saint Exupery.

I am associate professor at Ecole Nationale Supérieure d'Electrotechnique, Electronique, Informatique, Hydraulique et des Télécommunications (ENSEEIHT), a public engineering school part of Institut National Polytechnique de Toulouse (INPT), which is a member of the Pôle de Recherche et Enseignement Supérieur (PRES) Université de Toulouse.

Surface Mail: ENSEEIHT, Bureau F305, 2 rue Charles Camichel, 31071 TOULOUSE Cedex FRANCE

Electronic Mail: Marc dot Pantel at enseeiht dot fr

Phone +(33) 534 32 2185, Fax +(33) 534 32 2157, Professional Cellphone +(33) 676 221 687

• 2017/07/13: The DISCONT project has been funded by ANR.
• 2016/11/22-25: Attending the Implicit and Explicit semantics integration in proof based developments of discrete systems in Shonan, Tokyo, Japan.
• 2016/11/21: Attending the Event-B Day 2016 in Tokyo at NII in Tokyo, Japan.
• 2016/11/14-18: Attending the ICFEM'2016 conference in Tokyo, Japan.
• 2016/10/02-05: Attending the MODELS'2016 conference in Saint Malo, France (talk at EXE'2016 and MODEVVA'2016).
• 2016/09/27: Participation to the FMICS/AVOCS'2016 workshop in Pisa, Italia (talk at FMICS/AVOCS).
• 2016/08/16: Our contribution to EXE@MODELS'2016 has been accepted.
• 2016/08/15: Our contribution to MoDeVVa@MODELS'2016 has been accepted.
• 2016/06/29: Our contribution to ICFEM'2016 has been accepted.
• 2016/06/26: Our contribution to FMICS/AVOCS'2016 has been accepted.
• 2016/03/16-18: Last GEMOC project meeting in Paris, France.
• Older ones...

• Formal Software Engineering
• Model Driven Engineering for Safety Critical Systems
  • Domain Specific (Modeling) Language Semantics
  • Model transformation formal specification and verification
• Applied formal methods
  • Static analysis
  • Proof assistant
  • Model checking
  • Constraint solving

• Combining Object Oriented Programming and Pure Functional Programming, from 1990 to 1994
• Actor Languages Static Analysis, from 1994 to 2009
• Actor Languages implementation in CaML and Java, from 1999 to 2006
• Constraint Solver based Static Analysis, from 1990 to 2009
• Scientific Application Modeling, from 2002 to 2009

• IRIT Database
• DBLP
• Google Scholar

• Time properties dedicated semantics for uml-marte safety critical real-time system verification

• Block Library specification language (with Arnaud Dieumegard, Andres Toom and Guillaume Babin)
• RT-Fiacre xText grammar and metamodel (with Faiez Zalila)
• UML Real Time Verification Toolset (with Ning Ge)
• TOM backend for the Ada language
• Block sequencer for the GeneAuto toolset written in Java, CaML and Coq (with Nassima Izerrouken et Xavier Thirioux)

• 2016: ICMT, …
• 2015: TSI, ETFA, ICMT, …
• 2014: ICMT, MPM, ETFA, CAL, CIEL, GDR GPL, …
• 2013: ETFA, …
• To be completed

• Journal of Software and Systems
• Science of Computer Programming
• Formal Aspects Of Computing
• Software and Systems
• To be completed

• Mathieu Montin, started Q1 2014 (in cooperation with Xavier Crégut)
• Andres Toom, started Q4 2009 (in cooperation with Tarmo Uustaluu)

• Soukayna M'Sirdi, started Q1 2014 (in cooperation with Airbus Group Innovations)
• Guillaume Babin, started Q4 2013 (in cooperation with Yamine Aït Ameur)
• Florent Latombe: Systematic Use of Models of Concurrency in eXecutable Domain-Specific Modeling Languages (2012 to 2016, in cooperation with Xavier Crégut), Research & Development Engineer at OBEO; Toulouse, France
• Matteo Bordin: Model driven qualification process for safety critical system development tools started Q1 2012 (in cooperation with AdaCore as a an ongoing training) and stopped Q3 2015 (after moving from AdaCore to Criteo), Senior Product Manager at Criteo, Paris, France
• Arnaud Dieumegard: Formal guarantees for Safety Critical Code Generation: The case of highly variable languages (2011 to 2015), post-doctoral intern at the IRT Saint Exupery, France
• Faiez Zalila: Methods and Tools for the Integration of Formal Verification in Domain-Specific Languages (2010 to 2014, in cooperation with Xavier Crégut), post-doctoral intern at the IRT Saint Exupery, France
• Jean-Christophe Bach: Un îlot formel pour les transformations de modèles qualifiables , (2010 to 2014, in cooperation with Pierre-Etienne Moreau), Associate Professor at ENST-Bretagne, France
• Ning Ge: Property Driven Verification Framework: Application to Real-Time Property for UML-MARTE Software Designs (2010 to 2014, (in cooperation with Xavier Crégut), Research Engineer at Systerel, detached to the IRT Saint Exupery, France
• Mounira Kezadri: Validation et vérification de systèmes critiques: Ontologies et intégration de composants (2009 to 2013, in cooperation with Xavier Thirioux and Benoît Combemale), post-doctoral intern at Ottawa, Canada
• Ricardo Bedin França: Processes and qualifiable tools for the development of safety critical certified systems in avionics based on automated code generation (2009 to 2012, funded by Airbus), working as system engineer at Embraer in Brasil
• Nassima Izerrouken: Développement prouvé de composants formels pour un générateur de code embarqué critique pré-qualifié (2007 to 2011, in cooperation with Xavier Thirioux, funded by Continental Automotive), working as Research and Development engineer at Altran in France
• Benoît Combemale: Approche de métamodélisation pour la simulation et la vérification de modèle (2006 to 2009, in cooperation with Xavier Crégut and Xavier Thirioux), Associate Professor at Université de Rennes
• Pierre-Loïc Garoche: Analyse statique d'un calcul d'acteurs par interprétation abstraite (2006 to 2009, in cooperation with Xavier Thirioux), Research Associate at ONERA
• Aurélie Hurault: Courtage sémantique de services de calcul (2004 to 2007, in cooperation with Michel Daydé), Associate Professor at ENSEEIHT
• Vincent Hennebert, Computer Science Engineer, from 2004 to 2007 (in cooperation with Xavier Thirioux), FOP expert and developer at ThunderHead in London, United Kingdom
• Matthias Colin: Analyse statique de la communication dans un langage d'acteurs fonctionnel (1999 to 2003, in cooperation with Xavier Thirioux), Assistant Professor at EISTI
• Fabien Dagnat: Vérification statique de programmes répartis (1998 to 2001, in cooperation with Patrick Sallé), Associate Professor at ENST-Bretagne
• Jean-Louis Colaço: Analyses Statiques de Langages d'Acteurs par inférence de types (1994 to 1997, in cooperation with Patrick Sallé), Research and Development Engineer at Esterel Technologies

• 2016/09/26: Sangeeth Saagar Ponnusamy, Université de Toulouse/UPS (member)
• 2016/07/13: Florent Latombe, Université de Toulouse/INPT (advisor)
• 2015/04/03: Romain Jobredeau, Georgia Institute of Technology (member)
• 2015/04/03: Timothy Wang, Georgia Institute of Technology (member)
• 2015/01/30: Arnaud Dieumegard, Université de Toulouse/INPT (advisor)
• 2014/12/09: Faiez Zalila, Université de Toulouse/INPT (advisor)
• 2014/09/12: Jean-Christophe Bach, Université de Nancy (advisor)
• 2014/07/03: Cédrick Lelionnais, Université de Nantes (member)
• 2014/06/17: Andre Maroneze, Université de Rennes 1 (member)
• 2014/04/12: Ning Ge, Université de Toulouse/INPT (advisor)
• 2013/12/10: Clément Guy, Univ. Rennes 1 (member)
• 2013/07/11: Mounira Kezadri, Université de Toulouse/INPT (advisor)
• 2013/06/20: Matthieu Giorgino, Université de Toulouse/Université Paul Sabatier (invited)
• 2012/12/19: Quyet-Thang Pham, Telecom Bretagne (reviewer)
• 2012/04/10: Ricardo Bedin França, Université de Toulouse/INPT (advisor)
• 2011/07/06: Nassima Izerrouken, Université de Toulouse/INPT (advisor)
• 2009/12/10: Yann Glouche, Univ. Rennes 1 (member)
• 2009/07/06: Zianah Dargaye, Univ. Denis Diderot (member)
• 2008/06/10: Pierre-Loïc Garoche, Université de Toulouse/INPT (advisor)
• 2006/12/04: Aurélie Hurault, Université de Toulouse/INPT (advisor)
• 2003/12/15: Cyril Carrez, Telecom ParisTech (member)
• 2002/12/20: Matthias Colin, Université de Toulouse/INPT (advisor)
• 2001/05/28: Fabien Dagnat, Université de Toulouse/INPT (advisor)
• 1999/03/19: Abdelkrim Nimour, Telecom ParisTech (member)
• 1997/10/18: Jean-Louis Colaço, Université de Toulouse/INPT (advisor)

• ANR FORMEDICIS, 2017 to 2020
• RTRA STAE IFSE2, 2016 to 2018
• ANR IMPEX, 2013 to 2017, IMPlicit and EXplicit semantics in the development of critical systems
• ANR ASTRID VORACE, 2012 to 2016, End to end verification of optimization algorithms for control and command safety critical systems

• Safety critical systems
  • ANR INS GeMoC, 2012 to 2016, Heterogeneous Modeling based on Models of Computation
  • RTRA STAE TORRENTS, 2011 to 2014
  • RTRA STAE IFSE, 2011 to 2016
  • RTRA STAE BriefCase, 2012 to 2016
  • ITEA2 openETCS, 2011 to 2015, Application of TOPCASED technologies to the European Train Control Systems domain
  • FUI Projet P, 2011 to 2015, Intermediate languages and code generation for safety critical systems (GeneAuto and TOPCASED followup)
  • CrAVES collaborative French-USA project, Credible Autocoding and Verification of Embedded Software
  • EuroStars HiMoCo, 2011 to 2014, High Integrity Model Compiler
  • FRAE quarteFt, 2009 to 2012
  • ITEA2 OPEES, 2009 to 2012
  • ARTEMIS CESAR, 2010 to 2012
  • FUI TOPCASED, 2006 to 2010
  • ITEA GeneAuto, 2006 to 2008
  • ITEA ES_PASS, 2008 to 2010
  • ANR SPaCIFY, 2008 to 2010
• Distributed systems
  • ACI GRID-TLSE, 2002 to 2004
  • ANR LEGO, 2006 to 2008
  • ANR RNTL SCORWARE, 2007 to 2009

• Tarmo Uustalu, Cybernetics Institute, Tallinn Technical University, Estonia
• Eric Féron, Romain Jobredeaux, Timothy Wang, Georgia Institute of Technology, Atlanta, USA
• Heber Herencia-Zapana, National Institute of Aeronautics, Langley, USA
• Jean-Marie Farines, UFSC, Brasil

• Horaciu Cirstea, Pierre-Etienne Moreau (LORIA-PAREO) : TOM
• Jean-Pierre Talpin (IRISA-ESPRESSO) : PolyChrony
• Sandrine Blazy (IRISA-CELTIQUE), Xavier Leroy (INRIA) : CompCert
• Olivier Barais, Arnaud Blouin, Benoît Combemale, Didier Vojtisek (IRISA-TRISKELL) : Kermeta, GEMOC
• Julien De Antoni, Frédéric Malet (INRIA-AOSTE) : CCSL, ECL, TimeSquare, GEMOC
• François Vernadat, Bernard Berthomieu, Silvano Dal Zilio, Didier Le Botlan (LAAS) : Fiacre, Tina
• Virginie Wiels, Frédéric Boniol, David Doose, Pierre-Loïc Garoche (ONERA)

• Object Oriented Technologies: Java programming, UML design
• Formal Foundation of Computer Science: Propositional and Predicate Logic, Set Theory, Coq Proof Assistant, Hoare Logic, Why Toolset, Finite Automaton, Regular Expression, Non Contextual Grammar, Lex, Yacc

• Software and System Engineering: Advanced UML and SysML, Model Driven Engineering, Design Patterns
• Compilers and Formal Semantics: Recursive Descent Parsing, Attribute semantics, Type systems, Code generation, Operational semantics, Axiomatic semantics, Denotational semantics, Proof of static analyser and code generator correctness

• Model Driven Engineering
• Static Analysis based Verification of software
• Safety Critical Embedded Systems (SEC)

• Development of safety critical systems

• Model Driven Engineering

• Model Driven Engineering: Toolset

• Elected member of the ENSEEIHT management council
• Member of the Formal Method Forum (joint initiative from AeroSpace Valley and RTRA STAE)
• Member of the TISECA platform writing board in the AESE IRT
• Member of the ISAURE scientific board from the Aerospace Valley cluster
• Member of the Action IDM scientific board from the GDR GPL and GDR ASR
• Member of the EICOSE management board
• Expert for the Luxembourg FNR, French ANR, French D2RT

• Member of the INPT management board
• Member of the IRIT management board
• Member of the ENSEEIHT Computer Science and Applied Mathematics department council
• Designer and Manager of the INPT/ENSEEIHT Mastere in Technologies des Applications Multimédia
• Manager of the INPT/ENSEEIHT Mastere in Méthodes Avancées Appliquées à l'Informatique