Hubert Garavel    home         cv        publications      talks      academic     editorship     music     photos

Academic Activities

Lectures

1991-2000: course on Real Time at the ENSIMAG engineering school (Grenoble) in collaboration with Daniel Pilaud until 1993 and with Radu Mateescu in 1999 and 2000. This course is now taught by Frédéric Lang and Wendelin Serwe.

1993-1998: lab exercises in Specification and Validation of Protocols at ENST (Paris) in collaboration with Elie Najm and Arnaud Février.

1995-1997: lab exercises in Formal Description Techniques at ENSERG (Grenoble) in collaboration with Alain Kerbrat and Ghislaine Thuau.

1998-2000: creation of a master research course on Specification and Validation of Protocols at Université de Savoie (Annecy). This course was later taught by Frédéric Lang and Radu Mateescu.

2007-2011: creation of an engineering course on Formal Methods of Development at CNAM (Grenoble) in collaboration with Frédéric Lang, Pascal Raymond, and Wendelin Serwe.

2012: creation of a block course on Applied Concurrency Theory at Saarland University (Saarbrücken). Assistant: Alexander Graf-Brill.

2016-now: creation, together with Laurence Pierre, of the High-confidence Embedded and Cyberphysical Systems (HECS) curriculum for the 2nd-year students of MOSIG, the international master program in computer science, common to Grenoble INP and University Grenoble Alpes. .

2016: lectures on model-driven engineering and on the synchronous languages Lustre and SCADE, as part of the MOSIG/HECS-4 course on Industrial Processes for High-Confidence Design, in collaboration with Laurence Pierre and Ylies Falcone.

2016-2020: lectures on probabilistic models, stochastic models, and static/dynamic fault trees, as part of the MOSIG/HECS-3 course on Performance and Quantitative Properties, in collaboration with Thao Dang, Goran Frehse, Claire Maiza, and Sophie Quinton.

2021-2022: lectures on the challenges of embedded software design and the principles of LUSTRE/SCADE modelling, as part of the MOSIG course on Embedded Systems: From High-Confidence Design to Safe Execution, in collaboration with Ylies Falcone, Laurence Pierre, Pascal Raymond, and Wendelin Serwe.

2021-2023: lectures on probabilistic models, stochastic models, and static/dynamic fault trees, as part of the MOSIG course on System Design: Real-Time, Stochastic, and Analog/Digital, in collaboration with Thao Dang, Frédéric Lang, Claire Maiza, and Radu Mateescu.

Doctorate Students

Radu Mateescu. Vérification des propriétés temporelles des programmes parallèles. Thèse de Doctorat, Institut National Polytechnique de Grenoble, April 1998.

Mihaela Sighireanu. Contribution à la définition et à l'implémentation de la norme ``Extended LOTOS''. Thèse de Doctorat, Université Joseph Fourier (Grenoble), January 1999.

Damien Thivolle. Langages modernes pour la modélisation et la vérification des programmes asynchrones. Thèse de Doctorat, Université Polytechnique de Bucarest and Université Joseph Fourier (Grenoble), April 2011 (joint supervision with Valentin Cristea).

Raquel Oliveira. Vérification de systèmes interactifs. Thèse de Doctorat, Université Joseph Fourier (Grenoble), 2012-2016 (joint supervision with Sophie Dupuy-Chessa, with the collaboration of Gaëlle Calvary and Frédéric Lang).

Pierre Bouvier. Thèse de Doctorat, Université Joseph Fourier (Grenoble), 2019-now (joint supervision with Radu Mateescu).

Master Students

Juan Galvez Londono. Analyse du flux des données dans un système parallèle. DEA, Institut National Polytechnique de Grenoble, June 1993.

Radu Mateescu. Définition et compilation d'un méta-langage pour l'implémentation des logiques temporelles. DEA, Institut National Polytechnique de Grenoble and Université Joseph Fourier (Grenoble), June 1994.

Mihaela Sighireanu. Méthodes de représentation des types abstraits algébriques en vue de la vérification de protocoles. DEA, Institut National Polytechnique de Grenoble and Université Joseph Fourier (Grenoble), June 1995.

Manuel Aguilar Cornejo. Etude comparative et application des techniques de description formelle LOTOS et E-LOTOS à des protocoles pour les systèmes répartis. DEA, Institut National Polytechnique de Grenoble and Université Joseph Fourier (Grenoble), June 1999. (joint supervision with Radu Mateescu).

Jean-Philippe Gros. A Unifying Framework for Comparing and Implementing Probabilistic Models. MOSIG Master 2, Univ. Grenoble Alpes, June 2017.

Pierre Bouvier. Automated Discovery of Nested Units in Petri Nets. MOSIG Master 2, Univ. Grenoble Alpes, February-June 2019.

Engineering and Bachelor Students

Pascal Bouchon and Jean-Michel Houdouin. Analyseur LOTOS pour CAESAR. Mémoire d'ingénieur ENSIMAG, Laboratoire de Génie Informatique (Institut IMAG), Grenoble, June 1988.

Khalid Benabdelkader and Tarik Maaouni. Atelier Logiciel pour l'Analyse des Systèmes de Transitions. Mémoire d'ingénieur ENSIMAG, Laboratoire de Génie Informatique (Institut IMAG), Grenoble, June 1991.

Philippe Turlier. La compilation des types abstraits algébriques du langage LOTOS. Mémoire d'ingénieur CNAM, Grenoble, December 1992.

Radu Mateescu. Optimisation de la compilation des types abstraits algébriques du langage LOTOS. Mémoire d'ingénieur de l'Institut Polytechnique de Bucarest, September 1993.

Mihaela Sighireanu. Implémentation optimisée des types abstraits algébriques du langage LOTOS. Mémoire d'ingénieur de l'Institut Polytechnique de Bucarest, September 1994.

Renaud Ruffiot. Définition et réalisation d'un atelier logiciel pour l'étude des systèmes de transitions. Mémoire d'ingénieur CNAM, Grenoble, December 1994.

Louis-Pascal Tock. The BCG PostScript Format. Mémoire de stage ENSIMAG, INRIA Rhône-Alpes, October 1995.

Xavier Etchevers, Jean-Michel Frume, and Mark Jorgensen. De CAESAR a ELUDO : développement et intégration d'outils pour l'ingénierie des protocoles. Mémoire d'ingénieur ENSIMAG, INRIA Rhône-Alpes and University of Ottawa, June 1996.

Bruno Vivien. Etude du système SYNTAX/FNC-2 pour la génération de compilateurs. Mémoire de probatoire en informatique, CNAM, Grenoble, June 1996 (joint supervision with Mihaela Sighireanu).

David Jacquemin. Interconnexion des ateliers CADP et FC2Tools. Stage d'ingénieur ENSIMAG, Grenoble, August 1997.


Patrick Wendel. Réalisation d'un assistant automatique d'installation en Tcl/Tk. Stage d'ingénieur ENSIMAG, Grenoble, August 1997.


Bruno Vivien. Etude et réalisation d'un compilateur E-LOTOS à l'aide du générateur de compilateurs SYNTAX/FNC-2. Mémoire d'ingénieur, CNAM, Grenoble, December 1997 (joint supervision with Mihaela Sighireanu).

Bruno Hondelatte and Pierre Kessler. Réalisation d'un simulateur graphique pour applications parallèles et temps-réel. Mémoire d'ingénieur ENSIMAG, INRIA Rhône-Alpes, Grenoble, June 1998.

Jean Dina. Présentation du système de vérification SPIN. Mémoire de probatoire en informatique, CNAM, Grenoble, June 1998.

Aldo Mazzilli. Présentation du système de vérification MURPHI. Mémoire de probatoire en informatique, CNAM, Grenoble, June 1998.

Claude Chaudet. Compilation optimisée des types de données LOTOS, E-LOTOS et LOTOS NT. Mémoire d'ingénieur IEE-CNAM, INRIA Rhône-Alpes, Grenoble, June 1999.

Yan Uschanoff. Présentation du programme de vérification Verisoft. Mémoire de probatoire en informatique, CNAM, Grenoble, June 1999 (joint supervision with Radu Mateescu).

Aldo Mazzilli. Etude de la migration et de la portabilité des applications informatiques d'Unix vers Windows NT. Mémoire d'ingénieur, CNAM, Grenoble, December 1999.


Gilles Stragier. Prise en charge de systèmes de transitions étiquetées de grande taille - Utilisation d'un cache et d'un réseau d'ordinateurs. Mémoire de maîtrise en informatique, Université Libre de Bruxelles, September 2002 (joint supervision with Radu Mateescu).

Nathalie Lépy. Environnement de développement intégré sous Eclipse pour la vérification des systèmes concurrents. CNAM, Grenoble, 2006-2007 (joint supervision with Frédéric Lang).

Jérôme Fereyre. Conception et amélioration d'outils logiciels pour la vérification distribuée. Mémoire d'ingénieur, CNAM, Grenoble, December 2007.


Imad-Seddik Arrada. Comparaison des performances de divers moteurs de réécriture. Grenoble, June-July 2015.

Sai-Srikar Kasi. Development of the Traian 3.0 compiler. Grenoble, May-July 2016.

Mohammad-Ali Tabikh. Etude comparative des moteurs de réécriture et de la compilation du filtrage. MOSIG Master 1, Univ. Grenoble Alpes, February-July 2016.

Julie Parreaux. Panorama des modèles et outils de vérification pour les systèmes probabilistes. Stage de licence L3, Université de Rennes et ENS Rennes, May-July 2017.

Arthur Feyt. Evaluation des outils basés sur la réécriture de termes. MOSIG Master 1, Univ. Grenoble Alpes, February-June 2019.

Habilitation Jurys

Leila Kloul. From Performance Analysis to Performance Engineering: Some Ideas and Experiments. Habilitation à Diriger des Recherches, Université de Versailles-Saint-Quentin-en-Yvelines, December 2006.

Radu Mateescu. Composants génériques pour l'analyse des systèmes de transitions. Habilitation à Diriger des Recherches, Institut National Polytechnique de Grenoble, Septembre 2007.

David Lugato. Formaliser par la modélisation : Applications au calcul haute performance et à la génération de tests par exécution symbolique. Habilitation à Diriger des Recherches, Université de Bordeaux, Mars 2015.

Katell Morin-Allory. Assertions et conception matérielle. Habilitation à Diriger des Recherches, Université Grenoble Alpes, Novembre 2018.

PhD Jurys

Marcos Veloso Peixoto. Automates à contraintes arithmétiques et procédures d'évaluation ascendante de programmes logiques. Thèse de Doctorat, Université Pierre et Marie Curie (Paris), December 1994.

Christian Hernalsteen. Specification, Validation and Verification of Real-Time Systems in ET-LOTOS. Thèse de Doctorat, Université Libre de Bruxelles, June 1998.

Judi Romijn. Analysing Industrial Protocols with Formal Methods. PhD thesis, University of Twente (The Netherlands); October 1999.

Fabrice Baray. Contribution à l'intégration de la vérification de modèle dans le processus de conception codesign. Thèse de Doctorat, Université Blaise Pascal (Clermont-Ferrand), July 2001.

Lars-Åke Fredlund. A Framework for Reasoning about ERLANG Code. PhD thesis, Royal Institute of Technology (Sweden), September 2001.

Christophe Lohr. Contribution à la conception de systèmes temps-réel s'appuyant sur la technique de description formelle RT-LOTOS. Thèse de Doctorat, Institut National Polytechnique de Toulouse, December 2002.

Frédéric Tronel. Application des problèmes d'accord à la tolérance aux défaillances dans les systèmes distribués asynchrones. Thèse de Doctorat, Université de Rennes I, December 2003.

Jun Pang. Formal Verification of Distributed Systems. PhD thesis, Free University of Amsterdam (The Netherlands), October 2004.

Nestor Cataño Collado. Méthodes formelles pour la vérification des programmes Java. Thèse de Doctorat, Université Paris 7 - Denis Diderot, November 2004.

Christophe Joubert. Vérification distribuée à la volée de grands espaces d'états. Thèse de Doctorat, Institut National Polytechnique de Grenoble, December 2005.

Marie Lalire. Développement d'une algèbre de processus pour le calcul quantique. Thèse de Doctorat, Institut National Polytechnique de Grenoble, October 2006.

Tarek Sadani. Vers l'utilisation des réseaux de Petri temporels étendus pour la vérification de systèmes temps-réel décrits en RT-LOTOS. Thèse de Doctorat, Institut National Polytechnique de Toulouse, May 2007.

Hans Svensson. Verification of Distributed Erlang Programs using Testing, Model Checking and Theorem Proving. PhD thesis, Chalmers University of Technology, University of Gothenburg, April 2008.

Romain Bernard. Analyses de sûreté de fonctionnement multi-systèmes. PhD thesis, Université de Bordeaux, November 23, 2009.

Nicolas Coste. Vers la prédiction de performance de modèles compositionnels dans les architectures GALS. PhD thesis, Université de Grenoble, June 24, 2010.

Matthias Raffelsieper. Cell Libraries and Verification. PhD thesis, Eindhoven University of Technology, November 2, 2011.