Michael Blondin

I am a tenured associate professor of computer science at the Université de Sherbrooke and a member of its Research group on fundamental computer science (GRIF). My research lies around the intersection of theoretical computer science and formal methods. In particular, I study the foundations of formal verification with the intended goal of enabling a more reliable and rigorous development of systems. My interests revolve around algorithmic verification, automata theory, concurrent and distributed systems, computational complexity theory and logic.

Before joining the Université de Sherbrooke, I obtained a joint Ph.D. from the ENS Paris-Saclay and the Université de Montréal, and I worked as a postdoctoral fellow at the Technical University of Munich.

Publications

Books

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

Journals (peer-reviewed)

• Michael Blondin and 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 and Guillermo A. Pérez. Continuous One-Counter Automata. ACM Transactions on Computational Logic (TOCL), vol. 24, no. 3, 2023.    
• Michael Blondin and 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 and 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 and 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 and Philipp J. Meyer. Towards efficient verification of population protocols. Formal Methods in System Design (FMSD), 2021.    
• Michael Blondin, Alain Finkel and 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 and Pierre McKenzie. Handling Infinitely Branching Well-structured Transition Systems. Information and Computation, vol. 258, pp. 28–49, 2018.    
• Michael Blondin, Alain Finkel, Christoph Haase and 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 and Pierre McKenzie. Well Behaved Transition Systems. Logical Methods in Computer Science (LMCS), vol. 13, no. 3, 2017.      
• Michael Blondin, Andreas Krebs and Pierre McKenzie. The Complexity of Intersecting Finite Automata Having Few Final States. Computational Complexity, vol. 25, no. 4, pp. 775–814, 2016.      

Invited contributions

• 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 and Antonín Kučera. Black Ninjas in the Dark: Formal Analysis of Population Protocols. LICS 2018.      

International conference proceedings (peer-reviewed)

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

Preprints

• Michael Blondin, Michaël Cadilhac, Xin-Yi Cui, Philipp Czerner, Javier Esparza and Jakob Schulz. Weakly acyclic diagrams: A data structure for infinite-state symbolic verification. 2024.  

Theses

• Algorithmics and complexity of counter machines. Ph.D. thesis, ENS Cachan – Université Paris-Saclay and Université de Montréal, 2016.      
• Complexité raffinée du problème d'intersection d'automates. M.Sc. thesis, Université de Montréal, 2012.    
• Complexité du problème d'intersection d'automates. B.Sc. honour thesis, Université de Montréal, 2009.      

Tools

• FastForward: an efficient (un)reachability verifier for Petri nets.

  FastForward is a tool for efficiently (semi-)deciding the reachability and coverability problems in Petri nets. It relies on computationally lightweight over-approximations of Petri nets as distance oracles in infinite graph exploration algorithms such as A* and greedy best-first search. In particular, FastForward can prove reachability with minimal witnesses. Moreover, it supports weighted transitions. More details can be found in our TACAS 2021 paper.

  • Source code on GitHub
• Peregrine: a tool for the analysis of population protocols.

  Peregrine is a tool for the analysis and parameterized verification of population protocols, a model of distributed in which mobile anonymous agents interact stochastically to achieve a common task. The analysis features of Peregrine include manual step-by-step simulation; automatic sampling; statistics generation of average convergence speed; detection of incorrect executions through simulation; and formal verification of correctness. The first four features are supported for all protocols, while verification is supported for silent protocols, a large subclass of population protocols. More details can be found in our CAV 2018 and PODC 2017 papers.

  • Homepage of Peregrine
  • Source code on GitLab
• QCover: an efficient coverability verifier for discrete and continuous Petri nets.

  QCover is an implementation of a decision procedure for the Petri net coverability problem. The procedure uses reachability in continuous Petri nets as a pruning criterion inside a backward-coverability framework. The heart of the approach is a sophisticated encoding of continuous Petri net reachability into SMT which then enables QCover to use the SMT solver Z3. QCover can also be used to decide reachability and coverability in continuous Petri nets. More details can be found in our TOCL 2017 and TACAS 2016 papers.

  • Current version on GitHub
  • TACAS 2016 version (37.5 MB)

Talks

• The complexity of linear temporal verification for continuous counter systems  
  Chair for Foundations of Software Reliability and Theoretical Computer Science, Technical University of Munich, July 18, 2024, Garching, Germany.
• On reachability in subclasses of unordered data Petri nets  
  Infinite Automata: workshop on infinite-state systems, June 25, 2024, Warlity Wielkie, Poland.
• Algorithmic verification of infinite-state systems via relaxations  
  PhD Open lecture series, University of Warsaw, October 26–28, 2022, Warsaw, Poland.
• Separators in Continuous Petri Nets
  Automata theory group seminar, University of Warsaw, October 26, 2022, Warsaw, Poland.
• Formal analysis of crowd systems  
  International Workshop on Synthesis of Complex Parameters (SynCoP), April 2, 2022, Munich, Germany (online).
• Automata-based formal verification
  Guest lecturer (CSC344), DePaul University, June 2020, Chicago, USA (online).
• Machines à compteurs: de la calculabilité à la vérification de programmes  
  Mathematics Club, Université de Sherbrooke, October 31, 2019, Sherbrooke, Canada.
• Automatic analysis of population protocols  
  International Workshop on Multi-objective Reasoning in Verification and Synthesis (MoRe), June 22, 2019, Vancouver, Canada.
• Affine Extensions of Integer Vector Addition Systems with States  
  PaVeS Seminar, Technical University of Munich, May 28, 2019, Garching, Germany.
• Vérification algorithmique pour le développement de systèmes fiables  
  Computer Science Club, Université de Sherbrooke, November 21, 2018, Sherbrooke, Canada.
• – Affine Extensions of Integer Vector Addition Systems with States  
  – Automatic Analysis of Expected Termination Time for Population Protocols  
  CONCUR, September 7, 2018, Beijing, China.
• Formal Verification of Population Protocols
  Autobóz: workcamp on automata, logic and games theory, July 18, 2018, Gèdre, France.
• Formal Analysis of Population Protocols  
  Dagstuhl Seminar 18211 (Formal Methods and Fault-Tolerant Distributed Computing: Forging an Alliance), May 24, 2018, Wadern, Germany.
• Automatic Analysis of Expected Termination Time for Population Protocols  
  LSV Seminar, ENS Paris-Saclay, May 15, 2018, Cachan, France.
• On the State Complexity of Population Protocols  
  Verification Seminar, University of Oxford, March 29, 2018, Oxford, United Kingdom.
• – 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, March 16, 2018, Eichstätt, Germany.
• Vérification automatique de systèmes infinis
  Université de Sherbrooke, Computer science department, October 6, 2017, Sherbrooke, Canada.
• Reachability in VASS with Two Counters
  Autobóz: workcamp on automata, logic and games theory, July 22, 2017, Koninki, Poland.
• On Tools for Coverability  
  Gregynog 71717: Workshop on Vector Addition Systems, July 6, 2017, Tregynon, United Kingdom.
• Logics for Continuous Reachability in Petri Nets and Vector Addition Systems with States  
  LICS, June 20, 2017, Reykjavík, Iceland.
• Towards Efficient Verification of Population Protocols  
  Verification Seminar, University of Oxford, May 24, 2017, Oxford, United Kingdom.
• The Logical View on Continuous Petri Nets  
  PUMA Workshop, October 13, 2016, San Martino in Passiria, Italy.
• Approaching the Coverability Problem Continuously  
  PUMA Seminar, Technical University of Munich, May 11, 2016, Garching, Germany.
• Approaching the Coverability Problem Continuously  
  TACAS, April 6, 2016, Eindhoven, Netherlands.
• Reachability in Two-Dimensional Vector Addition Systems with States is PSPACE-complete  
  LICS, July 6, 2015, Kyoto, Japan.
• Reachability in Two-Dimensional Vector Addition Systems with States is PSPACE-complete  
  GT Verification Annual Days, June 15, 2015, Créteil, France.
• Reachability in Two-Dimensional Vector Addition Systems with States
  Automata theory group seminar, Warsaw University, May 18, 2015, Warsaw, Poland.
• Reachability in continuous vector addition systems: from theory to practice  
  INFINI Seminar, LSV, ENS Cachan, May 13, 2015, Cachan, France.
• Accessibilité dans les systèmes d’addition de vecteurs à deux compteurs  
  LITQ Seminar, Université de Montréal, February 14, 2015, Montreal, Canada.
• Handling Infinite Branching WSTS  
  ICALP, July 8, 2014, Copenhagen, Denmark.
• Handling Infinite Branching WSTS  
  DigiCosme Research Days, July 2, 2014, Orsay, France.
• Handling Infinite Branching WSTS  
  GT Verification Annual Days, June 16, 2014, Paris, France.
• Handling Infinite Branching WSTS  
  Dagstuhl Seminar 14141 (Reachability Problems for Infinite-State Systems), March 31, 2014, Wadern, Germany.
• Handling Infinite Branching WSTS  
  ReacHard Seminar, LaBRI, Université de Bordeaux, January 6, 2014, Talence, France.
• The Complexity of Intersecting Finite Automata Having Few Final States  
  INFINI Seminar, LSV, ENS Cachan, October 31, 2013, Cachan, France.
• The Complexity of Intersecting Finite Automata Having Few Final States  
  CSR, July 7, 2012, Nizhny Novgorod, Russia.

Teaching

• IFT436 – Algorithms and data structures: F24 | F23 | F22 | F21 | F20 | F19 (in French)
• IGL502/752 – Model checking: F24 | F23 | F22 | F21 | F20 | W19 (in French)
• IFT209 – System programming: W24 | W23 | W22 | W21 | W20 | W19 (in French)
• IFT503/711 – Theory of computation: W24 | W23 | W22 | W21 | W20 | W19 (in French)
• IFT769 – Selected topics in theoretical computer science (automata theory): W22 (in French)

Research team

Résumé (short version)

Contact

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

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

• Office D4-1024-1 (Building D4, 1^st floor)
  Faculté des sciences
  2500 boulevard de l'Université
  Sherbrooke (Québec), Canada

• Design adapted from HTML5 UP