Michael Blondin

Je suis professeur agrégé au Département d'informatique de l'Université de Sherbrooke et membre de son Groupe de recherche en informatique fondamentale (GRIF). Ma recherche se situe autour de l'intersection de l'informatique théorique et des méthodes formelles. En particulier, j'étudie les fondements de la vérification formelle dans le but de permettre un développement plus fiable et rigoureux des systèmes informatiques. Mes intérêts gravitent autour de la vérification algorithmique, de la théorie des automates, des systèmes concurrents et distribués, de la théorie de la complexité et de la logique.

Avant de me joindre à l'Université de Sherbrooke, j'ai obtenu un doctorat en cotutelle de l'ENS Paris-Saclay et de l'Université de Montréal, et j'ai également occupé un poste d'enseignant-chercheur postdoctoral à l'Université technique de Munich.

Notes de cours

Publications

Livres

• Javier Esparza et Michael Blondin. Automata Theory: An Algorithmic Approach. MIT Press, 2023.

Revues (évaluées par les pairs)

• Michael Blondin et Javier Esparza. Separators in Continuous Petri Nets. Logical Methods in Computer Science (LMCS), vol. 20, no. 1, 2024.      
• Michael Blondin, Tim Leys, Filip Mazowiecki, Philip Offtermatt et Guillermo A. Pérez. Continuous One-Counter Automata. ACM Transactions on Computational Logic (TOCL), vol. 24, no. 3, 2023.    
• Michael Blondin et Mikhail Raskin. The Complexity of Reachability in Affine Vector Addition Systems with States. Logical Methods in Computer Science (LMCS), vol. 17, no. 3, 2021.      
• Michael Blondin, Christoph Haase, Filip Mazowiecki et Mikhail Raskin. Affine Extensions of Integer Vector Addition Systems with States. Logical Methods in Computer Science (LMCS), vol. 17, no. 3, 2021.      
• Michael Blondin, Matthias Englert, Alain Finkel, Stefan Göller, Christoph Haase, Ranko Lazić, Pierre McKenzie et Patrick Totzke. The Reachability Problem for Two-Dimensional Vector Addition Systems with States. Journal of the ACM (JACM), vol. 68, no. 5, pp. 34:1–34:43, 2021.    
• Michael Blondin, Javier Esparza, Stefan Jaax et Philipp J. Meyer. Towards efficient verification of population protocols. Formal Methods in System Design (FMSD), 2021.    
• Michael Blondin, Alain Finkel et Jean Goubault-Larrecq. Forward Analysis for WSTS, Part III: Karp-Miller Trees. Logical Methods in Computer Science (LMCS), vol. 16, no. 2, 2020.      
• Michael Blondin, Alain Finkel et Pierre McKenzie. Handling Infinitely Branching Well-structured Transition Systems. Information and Computation, vol. 258, pp. 28–49, 2018.    
• Michael Blondin, Alain Finkel, Christoph Haase et Serge Haddad. The Logical View on Continuous Petri Nets. ACM Transactions on Computational Logic (TOCL), vol. 18, no. 3, pp. 24:1–24:28, 2017.      
• Michael Blondin, Alain Finkel et Pierre McKenzie. Well Behaved Transition Systems. Logical Methods in Computer Science (LMCS), vol. 13, no. 3, 2017.      
• Michael Blondin, Andreas Krebs et Pierre McKenzie. The Complexity of Intersecting Finite Automata Having Few Final States. Computational Complexity, vol. 25, no. 4, pp. 775–814, 2016.      

Contributions invitées

• Michael Blondin. The ABCs of Petri net reachability relaxations. ACM SIGLOG News: verification column, vol. 7, no. 3, 2020.    
• Michael Blondin, Javier Esparza, Stefan Jaax et Antonín Kučera. Black Ninjas in the Dark: Formal Analysis of Population Protocols. LICS 2018.      

Actes de conférences internationales (évalués par les pairs)

• Michael Blondin, Michaël Cadilhac, Xin-Yi Cui, Philipp Czerner, Javier Esparza et Jakob Schulz. Weakly acyclic diagrams: A data structure for infinite-state symbolic verification. TACAS 2025.    
• Michael Blondin, Alain Finkel, Piotr Hofman, Filip Mazowiecki et Philip Offtermatt. Soundness of reset workflow nets. LICS 2024.    
• Michael Blondin et François Ladouceur. Population Protocols with Unordered Data. ICALP 2023.      
• Michael Blondin, Philip Offtermatt et Alex Sansfaçon-Buchanan. Verifying linear temporal specifications of constant-rate multi-mode systems. LICS 2023.      
• Michael Blondin, Filip Mazowiecki et Philip Offtermatt. Verifying Generalised and Structural Soundness of Workflow Nets via Relaxations. CAV 2022.      
• Michael Blondin, Filip Mazowiecki et Philip Offtermatt. The complexity of soundness in workflow nets. LICS 2022.      
• Michael Blondin et Javier Esparza. Separators in Continuous Petri Nets. FoSSaCS, 2022.    
• Michael Blondin, Tim Leys, Filip Mazowiecki, Philip Offtermatt et Guillermo A. Pérez. Continuous One-Counter Automata. LICS, 2021.      
• Michael Blondin, Christoph Haase et Philip Offtermatt. Directed Reachability for Infinite-State Systems. TACAS 2021.      
• Michael Blondin et Mikhail Raskin. The Complexity of Reachability in Affine Vector Addition Systems with States. LICS 2020.      
• Michael Blondin, Javier Esparza, Martin Helfrich, Antonín Kučera et Philipp J. Meyer. Checking Qualitative Liveness Properties of Replicated Systems with Stochastic Scheduling. CAV 2020.      
• Michael Blondin, Javier Esparza, Blaise Genest, Martin Helfrich et Stefan Jaax. Succinct Population Protocols for Presburger Arithmetic. STACS 2020.      
• Michael Blondin, Javier Esparza et Stefan Jaax. Expressive Power of Broadcast Consensus Protocols. CONCUR 2019.      
• Michael Blondin, Christoph Haase et Filip Mazowiecki. Affine Extensions of Integer Vector Addition Systems with States. CONCUR 2018.      
• Michael Blondin, Javier Esparza et Antonín Kučera. Automatic Analysis of Expected Termination Time for Population Protocols. CONCUR 2018.          
• Michael Blondin, Javier Esparza et Stefan Jaax. Peregrine: A Tool for the Analysis of Population Protocols. CAV 2018.    
• Michael Blondin, Javier Esparza et Stefan Jaax. Large Flocks of Small Birds: On the Minimal Size of Population Protocols. STACS 2018.      
• Michael Blondin, Alain Finkel et Jean Goubault-Larrecq. Forward Analysis for WSTS, Part III: Karp-Miller Trees. FSTTCS 2017.      
• Michael Blondin, Javier Esparza, Stefan Jaax et Philipp J. Meyer. Towards Efficient Verification of Population Protocols. PODC 2017.        
• Michael Blondin et Christoph Haase. Logics for Continuous Reachability in Petri Nets and Vector Addition Systems with States. LICS 2017.      
• Michael Blondin, Alain Finkel, Christoph Haase et Serge Haddad. Approaching the Coverability Problem Continuously. TACAS 2016.          
• Michael Blondin, Alain Finkel, Stefan Göller, Christoph Haase et Pierre McKenzie. Reachability in Two-Dimensional Vector Addition Systems with States is PSPACE-complete. LICS 2015.        
• Michael Blondin, Alain Finkel et Pierre McKenzie. Handling Infinitely Branching WSTS. ICALP 2014.      
• Michael Blondin et Pierre McKenzie. The Complexity of Intersecting Finite Automata Having Few Final States. CSR 2012.      

Thèses et mémoires

• Algorithmique et complexité des systèmes à compteurs. Thèse de doctorat (Ph.D.), ENS Cachan – Université Paris-Saclay et Université de Montréal, 2016.      
• Complexité raffinée du problème d'intersection d'automates. Mémoire de maîtrise (M.Sc.), Université de Montréal, 2012.    
• Complexité du problème d'intersection d'automates. Mémoire de baccalauréat honor (B.Sc.), Université de Montréal, 2009.      

Outils

• FastForward: un outil efficace pour vérifier l'(in)accessibilité dans les réseaux de Petri.

  FastForward est un outil qui permet de (semi-)décider efficacement les problèmes d'accessibilité et de couverture des réseaux de Petri. Il s'appuie sur des sur-approximations d'accessibilité comme oracles de calcul de distance dans des algorithmes de parcours de graphes infinis comme A* et greedy-best search. FastForward est notamment en mesure de prouver l'accessibilité à l'aide de contre-exemples minimaux. De plus, il supporte les transitions pondérées. Pour plus de détails, voir l'article TACAS 2021.

  • Code source sur GitHub
• Peregrine: un outil pour l'analyse formelle des protocoles de populations.

  Peregrine est un outil pour l'analyse et la vérification paramétrée des protocoles de populations, un modèle de calcul distribué dans lequel des agents anonymes et mobiles interagissent de façon stochastique afin d'accomplir une tâche commune. Les fonctionnalités de Peregrine incluent la simulation manuelle pas-à-pas; l'échantillonnage automatique; la génération de statistiques sur le temps de convergence; la détection d'exécutions erronées via simulation; et la vérification formelle de correction. Les quatre premières fonctionnalités sont supportées pour tous les protocoles, et la vérification est supportée pour les protocoles silencieux, une grande sous-classe de protocoles de populations. Pour plus de détails, voir les articles CAV 2018 et PODC 2017.

  • Page Web de Peregrine
  • Code source sur GitLab
• QCover: un outil efficace pour la vérification des réseaux de Petri continus et discrets.

  QCover est une implémentation d'une procédure qui permet de décider le problème de couverture pour les réseaux de Petri. Cette procédure utilise l'accessibilité dans les réseaux de Petri continus comme critère d'élagage dans le cadre d'un algorithme d'exploration arrière. Le cœur de l'approche repose sur un traduction logique de l'accessibilité continue dans le solveur SMT Z3. QCover peut également être utilisé pour décider l'accessibilité et la couverture dans les réseaux de Petri continus. Pour plus de détails, voir les articles TOCL 2017 et TACAS 2016.

  • Code source sur GitHub

Présentations

• My Humble Journey Through Academia
  ETAPS Mentoring Workshop, 4 mai 2025, Hamilton, Canada.
• The complexity of linear temporal verification for continuous counter systems  
  Chair for Foundations of Software Reliability and Theoretical Computer Science, Université technique de Munich, 18 juillet 2024, Garching, Allemagne.
• On reachability in subclasses of unordered data Petri nets  
  Infinite Automata: workshop on infinite-state systems, 25 juin 2024, Warlity Wielkie, Pologne.
• Algorithmic verification of infinite-state systems via relaxations  
  PhD Open lecture series, Université de Varsovie, 26–28 octobre 2022, Varsovie, Pologne.
• Separators in Continuous Petri Nets
  Automata theory group seminar, Université de Varsovie, 26 octobre 2022, Varsovie, Pologne.
• Formal analysis of crowd systems  
  International Workshop on Synthesis of Complex Parameters (SynCoP), 2 avril 2022, Munich, Allemagne (en ligne).
• Automata-based formal verification
  Cours invité (CSC344), DePaul University, juin 2020, Chicago, États-Unis (en ligne).
• Machines à compteurs: de la calculabilité à la vérification de programmes  
  Club mathématique, Université de Sherbrooke, 31 octobre 2019, Sherbrooke, Canada.
• Automatic analysis of population protocols  
  International Workshop on Multi-objective Reasoning in Verification and Synthesis (MoRe), 22 juin 2019, Vancouver, Canada.
• Affine Extensions of Integer Vector Addition Systems with States  
  PaVeS Seminar, Université technique de Munich, 28 mai 2019, Garching, Allemagne.
• Vérification algorithmique pour le développement de systèmes fiables  
  Club informatique, Université de Sherbrooke, 21 novembre 2018, Sherbrooke, Canada.
• – Affine Extensions of Integer Vector Addition Systems with States  
  – Automatic Analysis of Expected Termination Time for Population Protocols  
  CONCUR, 7 septembre 2018, Pékin, Chine.
• Formal Verification of Population Protocols
  Autobóz: workcamp on automata, logic and games theory, 18 juillet 2018, Gèdre, France.
• Formal Analysis of Population Protocols  
  Dagstuhl Seminar 18211 (Formal Methods and Fault-Tolerant Distributed Computing: Forging an Alliance), 24 mai 2018, Wadern, Allemagne.
• Automatic Analysis of Expected Termination Time for Population Protocols  
  Séminaire du LSV, ENS Paris-Saclay, 15 mai 2018, Cachan, France.
• On the State Complexity of Population Protocols  
  Verification Seminar, University of Oxford, 29 mars 2018, Oxford, Royaume-Uni.
• – On the Analysis of Population Protocols  
  – Logics for Continuous Reachability in Petri Nets and Vector Addition Systems with States  
  Annual Seminar of the Chair for Foundations of Software Reliability and Theoretical Computer Science, 16 mars 2018, Eichstätt, Allemagne.
• Vérification automatique de systèmes infinis
  Université de Sherbrooke, Département d'informatique, 6 octobre 2017, Sherbrooke, Canada.
• Reachability in VASS with Two Counters
  Autobóz: workcamp on automata, logic and games theory, 22 juillet 2017, Koninki, Pologne.
• On Tools for Coverability  
  Gregynog 71717: Workshop on Vector Addition Systems, 6 juillet 2017, Tregynon, Royaume-Uni.
• Logics for Continuous Reachability in Petri Nets and Vector Addition Systems with States  
  LICS, 20 juin 2017, Reykjavik, Islande.
• Towards Efficient Verification of Population Protocols  
  Verification Seminar, University of Oxford, 24 mai 2017, Oxford, Royaume-Uni.
• The Logical View on Continuous Petri Nets  
  PUMA Workshop, 13 octobre 2016, San Martino in Passiria, Italie.
• Approaching the Coverability Problem Continuously  
  PUMA Seminar, Université technique de Munich, 11 mai 2016, Garching, Allemagne.
• Approaching the Coverability Problem Continuously  
  TACAS, 6 avril 2016, Eindhoven, Pays-Bas.
• Reachability in Two-Dimensional Vector Addition Systems with States is PSPACE-complete  
  LICS, 6 juillet 2015, Kyoto, Japon.
• Reachability in Two-Dimensional Vector Addition Systems with States is PSPACE-complete  
  Journées annuelles du GT-Verif, 15 juin 2015, Créteil, France.
• Reachability in Two-Dimensional Vector Addition Systems with States
  Automata theory group seminar, Université de Varsovie, 18 mai 2015, Varsovie, Pologne.
• Reachability in continuous vector addition systems: from theory to practice  
  Séminaire INFINI, LSV, ENS Cachan, 13 mai 2015, Cachan, France.
• Accessibilité dans les systèmes d’addition de vecteurs à deux compteurs  
  Séminaire du LITQ, Université de Montréal, 14 février 2015, Montréal, Canada.
• Handling Infinite Branching WSTS  
  ICALP, 8 juillet 2014, Copenhague, Danemark.
• Handling Infinite Branching WSTS  
  Journées Recherche DigiCosme, 2 juillet 2014, Orsay, France.
• Handling Infinite Branching WSTS  
  Journées annuelles du GT-Verif, 16 juin 2014, Paris, France.
• Handling Infinite Branching WSTS  
  Dagstuhl Seminar 14141 (Reachability Problems for Infinite-State Systems), 31 mars 2014, Wadern, Allemagne.
• Handling Infinite Branching WSTS  
  Séminaire ReacHard, LaBRI, Université de Bordeaux, 6 janvier 2014, Talence, France.
• The Complexity of Intersecting Finite Automata Having Few Final States  
  Séminaire INFINI, LSV, ENS Cachan, 31 octobre 2013, Cachan, France.
• The Complexity of Intersecting Finite Automata Having Few Final States  
  CSR, 7 juillet 2012, Nijni Novgorod, Russie.

Enseignement

• IFT503/711 – Théorie du calcul: H25 | H24 | H23 | H22 | H21 | H20 | H19
• IFT436 – Algorithmes et structures de données: A24 | A23 | A22 | A21 | A20 | A19
• IGL502/752 – Techniques de vérification et de validation: A24 | A23 | A22 | A21 | A20 | H19
• IFT209 – Programmation système: H24 | H23 | H22 | H21 | H20 | H19
• IFT769 – Sujets choisis en informatique théorique (théorie des automates): H22

Équipe de recherche

Curriculum vitæ (version courte)

Contact

• michael.blondinusherbrooke.ca
• (+1) 819-821-8000 poste 66491

• Michael Blondin
  Département d'informatique
  Université de Sherbrooke
  2500 boulevard de l'Université
  Sherbrooke (Québec), J1K 2R1, Canada

• Bureau D4-1024-1 (Pavillon D4, 1^er étage)
  Faculté des sciences
  2500 boulevard de l'Université
  Sherbrooke (Québec), Canada

• Design adapté de HTML5 UP