Thierry Jéron

Contact Address: IRISA / INRIA Rennes Campus Universitaire de Beaulieu 35042 Rennes Cedex - FRANCE e-mail: Thierry dot Jeron@inria.fr Tel: +33 2 99 84 74 64         +33 6 07 14 24 61 (mobile) Fax: +33 2 99 84 71 71 Secretary: +33 2 99 84 74 84 (Laurence Dinh )

Brief Biography

After studying Mathematics at the University of Rennes 1, I obtained a master (1988) and a  Ph.D. in Computer Science (1991) in the IRISA/INRIA laboratory, in the ADP team, under the supervision of Claude Jard and Michel Raynal. 
From 1991 to 1992, I was a research engineer in the Alcatel research lab in Marcoussis near Paris.
In 1993, I came back to IRISA/INRIA as an INRIA research scientist (Chargé de recherche) in the Pampa team where I did my research work for 8 years.
I obtained my Habilitation from University of Rennes 1 in March 2004 (text , video , slides).
From 2001 to 2012, I was the scientific leader of the VerTeCS team.
From 2011 to 2015, I was the Vice-Chairman of the projects committee of Inria Rennes - Bretagne Atlantique and member of the Inria Evaluation Committee.
From 2013 to 2023, I was a member of the SUMO Irisa/Inria team.
Since 2024, I am a member of the DEVINE Irisa/Inria team headed by Nathalie Bertrand.






Research Topics

My research topics concern the formal verification and  validation of large and reactive systems:

• Verification of large distributed systems.
• Verification, testing, learning of timed systems.
• Model-based testing: models and theory for conformance testing of reactive systems, automated test case synthesis with symbolic techniques for diverse models, with data, time, recursion.
• Diagnosis of Discrete Event Systems: models, theories, algorithms for the construction of diagnosers, verification of diagnosability.
• Monitoring and enforcement of timed properties.
• Security: security testing, diagnosis for intrusion detection.
• Verification of asynchronous communicating systems with approximate analysis.




Publications

Complete list of publications

• TGV is a test generation tool for models of labelled transition systems (LTS). The generation of test cases is guided by a test purpose (an automaton) and is based on "on-the-fly" co-reachability analysis of enumerated transition systems.
  
• STG is a test generation tool for models of transition systems extended with data variables and parameters (STS). Test generation from a system model and a test purpose is based on syntactic transformations of STS using approximate analysis (provided by the NBAC tool).

Responsibilities

• Steering committee
  
  • MOVEP Summer Schools (MOdelling and VErifying parallel Processes): MOVEP 2016 (DIBRIS, Università di Genova), MOVEP 2014 (IRCCyN, Nantes), MOVEP 2012 (CIRM, Marseille), MOVEP 2010 (RWTH Aachen), MOVEP 2008 (Orléans), MOVEP 2006 (Labri, Bordeaux), MOVEP 2004 (ULB, Bruxelles)
• PC membership
  
  • SAC-SVT 2022
  • ICTSS 2021, SAC-SVT 2021
  • ICTSS 2020, SAC-SVT 2020
  • ICTSS 2019, SAC-SVT 2017
  • SAC-SVT 2018
  • SAC-SVT 2017
  • ICTSS 2016, RV 2016
  • ICTSS 2015, TAP 2015, USE 2015
  • ICTSS 2014, TAP 2014, WODES 2014
  • TAP 2013 (Budapest, Hungary), RV 2013 (Rennes, France)
  • ICTSS 2012, ICFEM 2012, TAP 2012
  • ICST 2012, ICTSS 2012, ICFEM 2012, TAP 2012
  • ICTSS 2011, ICFEM 2011, SCENARIOS 2011, TAP 2011
  • ICTSS 2010, ICFEM 2010, QUATIC 2010
  • ICFEM 2009, TESTCOM/FATES 2009, SARSSI 2009
  • ICST 2008, TESTCOM/FATES 2008
  • Rosatea 2007
  • TACAS 2006 (Tool chair, Vienna, Austria), Testcom 2006 (New-York), Rosatea 2006 (Portland, Maine, USA)
  • Tacas 2005 (Edinburgh, Scotland, UK), Fates 2005 (Edinburgh, Scotland, UK), Testcom 2005 (Montréal, Quebec)
  • Fates 2004 (Linz, Austria) Testcom 2004 (Oxford, UK)
  • Fates 2003 (Montréal, Canada)
  • Fates 2002 (Co-chair, Brno, Czech Republic)
  • Fates 2001 (Aalborg, Denmark)
  • LFM 2000 (Williamsburg,Virginia, USA)
• Other
  
  • Dagstuhl Seminar on Symbolic Methods in Testing (Jan. 2013, co-organized with M. Veanes, B. Wolff)




Projects

• Current:
• ANR project PaVeDyS (2024-2027): Parametric Verification of Dynamic Distributed Systems.
• DST/Inria Associate Team SINCRET (2024-2026) : Scalable and incremental security monitoring and enforcement for timed systems with IIT Bhubaneswar (India).
• Project with Mitsubishi Electric Research Center Europe (MERCE) (2019-2024), Efficient Techniques and Tools for the Verification and Synthesis of Real-Time Systems
• Recent:
• ANR TickTac (2019-2023), Efficient Techniques and Tools for the Verification and Synthesis of Real-Time Systems
• IPL HAC-SPECIS (2016-2018), High-performance Application and Computers, Studying PErformance and Correctness In Simulation
• ANR Project Vacsim (2011-2015), Validation of control-command systems by coupling simulation and formal analysis
• ANR Project Testec (2008-2011), Test generation from models of real-time embedded systems
• NoE Artist 2 (2004-2008), Network of Excellence on Embedded Systems Design, Testing & Verification Cluster
• RNRT Politess (2006-2008), Security Policies for Network Information Systems: Modeling, Deployment, Testing and Supervision
• CRE France Telecom (2004-2006), Testing of Voice Services
• ACI Security Potestat (2004-2006), Security policies : test directed analysis of open network systems
• ACI Securité V3F (2003-2005), Validation and Verification of programs with floating point numbers
• UIUC/CNRS/INRIA collaboration (2005-2006), with Urbana Champain, Verimag, Runtime verification, monitoring, conformance testing and diagnosis




Teaching

I do not teach anymore, but I did in the past:

• University of Rennes 1, Master 2 Research in Computer Science (2002-2012): Model-based testing.
  
• University of Rennes 1, Master 2 Research in Computer Science (2000-2002): Computability and Complexity
• University of Rennes 1, Diic 3 (Engineers) (1994-2003): Protocol validation, model-checking and testing.
• EnstB Engineer School, Rennes, 3rd year (94-2005): Protocol validation, model-checking, testing
• EnstB Engineer School,  Brest, 2nd year (2001-2004): Model-based testing
• 3xI Engineer School, Brest (95-96): Protocol validation




PhD Students

Current:
• Mathieu Laurent (2023- ), with M. Quinson ) : Efficient verification of distributed asynchronous programs.
Past:
• Emily Clément (2018-2022, with N. Markey ) : Robustness of timed automata : computing the maximally-permissive strategies, currently ATER at IRIF.
• Léo Henry (2018-2021, with N. Markey ) : There and back again : formal methods and model learning for real-time systems : acting upon reality and learning from its reactions, currently Post Doc at University College London.
• Pham The Anh (2016-2019, with M. Quinson ) : Dynamic Formal Verification of High Performance Runtimes and Applications, now Engineer at Prover
• Paulin Fournier (2012-2015), with N. Bertrand ) : Parameterized verification of networks of many identical processes, now engineer at Clearsy
• Srinivas Pinisetty (2011-2015, with H. Marchand ) : Runtime enforcement of timed properties, now Assistant Professor at Indian Institute of Technology Bhubaneswar, India
• Amélie Stainer (2010-2013, with N. Bertrand ) : Quantitative verification of timed automata, now teacher
• Sébastien Chédor (2009-2014, with C. Morvan ) : Testing and diagnosis from recursive tile systems
• Jérémy Dubreil (2006-2009, with H. Marchand ) : Monitoring and Supervisory Control for Opacity, Software Engineer at Lacework
• Hatem Hamdi (2005-2008, with H. Marchand ): Compositional test generation
• Camille Constant (2004-2008, with V. Rusu , B. Jeannet ): Automatic test generation from models with variables and recursion, Assistant Professor at ESEO Angers
• Tristan Le Gall (2004-2008, with B. Jeannet ), Engineer, CEA, Saclay
• Valery Tschaen (2001-2005, with H. Marchand ): Control synthesis and conformance testing, teacher.
• Elena Zinovieva-Leroux (2000-2004, with V. Rusu ): Symbolic test generation for reactive systems with data, Assistant Professor at Université Bretagne Sud
• Pierre Morel (96-2000): Efficient algorithms for the generation of conformance tests.
• Yves-Marie Quemener (93-96): Verification of protocols with infinite state spaces using graph grammars, Orange Labs team manager, Lannion.