Aller au contenu
Trouver un autre spécialiste

Michael Blondin

Professeur, Faculté des sciences
FSCI Département d'informatique

Présentation

Sujets, disciplines ou intérêts de recherche

formal verification, automata theory, infinite state systems, model checking, computational complexity theory, logic

Diplômes

  • (2013-2016). Ph.D. in computer science (joint). École Normale Supérieure de Cachan. Cachan, Île-de-France, France.
  • (2012-2016). Ph.D. in computer science (joint). Université de Montréal. Montréal, QC, Canada.
  • (2010-2012). Master's (M.Sc.) in computer science. Université de Montréal. Montréal, QC, Canada.
  • (2007-2009). Bachelor's (B.Sc.) in computer science. Université de Montréal. Montréal, QC, Canada.
  • (2004-2007). College diploma (DEC) in computer science. Collège Lionel-Groulx. Sainte-Thérèse, QC, Canada.

Expériences académiques

  • Associate professor (tenured). (2023-). Université de Sherbrooke. Sherbrooke, Canada.
  • Assistant professor. (2018-2023). Université de Sherbrooke. Sherbrooke, QC, Canada.
  • Postdoctoral researcher. (2016-2018). Technical University Munich. Munich, Allemagne.

Publications

Articles

  • Michael Blondin, Javier Esparza. (2024). Separators in Continuous Petri Nets. Logical Methods in Computer Science (LMCS). DOI
  • Michael Blondin, Tim Leys, Filip Mazowiecki, Philip Offtermatt, Guillermo A. Pérez. (2023). Continuous One-Counter Automata. ACM Transactions on Computational Logic (TOCL). DOI
  • (2021). Affine Extensions of Integer Vector Addition Systems with States. Logical Methods in Computer Science (LMCS). DOI
  • (2021). The Complexity of Reachability in Affine Vector Addition Systems with States. Logical Methods in Computer Science (LMCS). DOI
  • (2021). The Reachability Problem for Two-Dimensional Vector Addition Systems with States. Journal of the ACM (JACM). DOI
  • (2021). Towards efficient verification of population protocols. Formal Methods in System Design (FMSD). DOI
  • (2020). Forward Analysis for WSTS, Part III: Karp-Miller Trees. Logical Methods in Computer Science (LMCS). DOI
  • (2020). The ABCs of Petri net reachability relaxations. ACM SIGLOG News. DOI
  • (2018). Handling infinitely branching well-structured transition systems. Information and Computation. DOI
  • (2017). The Logical View on Continuous Petri Nets. ACM Transactions on Computational Logic (TOCL). DOI
  • (2017). Well Behaved Transition Systems. Logical Methods in Computer Science. DOI
  • (2016). The complexity of intersecting finite automata having few final states. Computational Complexity. DOI

Livres

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

Articles de conférence

  • Michael Blondin, Alain Finkel, Piotr Hofman, Filip Mazowiecki, Philip Offtermatt. (2024). Soundness of reset workflow nets. Proc. 39th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). DOI
  • Michael Blondin, François Ladouceur. (2023). Population Protocols with Unordered Data. Proc. 50th EATCS International Colloquium on Automata, Languages and Programming (ICALP). DOI
  • Michael Blondin, Philip Offtermatt, Alex Sansfaçon-Buchanan. (2023). Verifying linear temporal specifications of constant-rate multi-mode systems. Proc. 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). DOI
  • (2022). Separators in Continuous Petri Nets. Proc. 25th International Conference on Foundations of Software Science and Computation Structure (FoSSaCS). DOI
  • Michael Blondin. (2022). The complexity of soundness in workflow nets. Proc. 37th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). DOI
  • Michael Blondin. (2022). Verifying Generalised and Structural Soundness of Workflow Nets via Relaxations. Proc. 34th International Conference on Computer Aided Verification (CAV). DOI
  • (2021). Continuous One-Counter Automata. Proc. 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). DOI
  • (2021). Directed Reachability for Infinite-State Systems. Proc. 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). DOI
  • (2020). Checking Qualitative Liveness Properties of Replicated Systems with Stochastic Scheduling. Proc. 32nd International Conference on Computer-Aided Verification (CAV). DOI
  • (2020). Succinct Population Protocols for Presburger Arithmetic. Proc. 37th Symposium on Theoretical Aspects of Computer Science (STACS). DOI
  • (2020). The Complexity of Reachability in Affine Vector Addition Systems with States. Proc. 35th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). DOI
  • (2019). Expressive Power of Broadcast Consensus Protocols. Proc. 30th International Conference on Concurrency Theory (CONCUR). DOI
  • (2018). Affine Extensions of Integer Vector Addition Systems with States. Proc. 29th International Conference on Concurrency Theory (CONCUR). DOI
  • (2018). Automatic Analysis of Expected Termination Time for Population Protocols. Proc. 29th International Conference on Concurrency Theory (CONCUR). DOI
  • (2018). Black Ninjas in the Dark: Formal Analysis of Population Protocols. Proc. 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). DOI
  • (2018). Large Flocks of Small Birds: On the Minimal Size of Population Protocols. Proc. 35th Symposium on Theoretical Aspects of Computer Science (STACS). DOI
  • (2018). Peregrine: A Tool for the Analysis of Population Protocols. Proc. 30th International Conference on Computer Aided Verification (CAV). DOI
  • (2017). Forward Analysis for WSTS, Part III: Karp-Miller Trees. Proc. 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS). DOI
  • (2017). Logics for Continuous Reachability in Petri Nets and Vector Addition Systems with States. Proc. 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). DOI
  • (2017). Towards Efficient Verification of Population Protocols. Proc. 36th ACM Symposium on Principles of Distributed Computing (PODC). DOI
  • (2016). Approaching the Coverability Problem Continuously. Proc. 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). DOI
  • (2015). Reachability in Two-Dimensional Vector Addition Systems with States Is PSPACE-Complete. Proc. 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). DOI
  • (2014). Handling Infinitely Branching WSTS. Proc. 41st International Colloquium on Automata, Languages, and Programming (ICALP). DOI
  • (2012). The Complexity of Intersecting Finite Automata Having Few Final States. Proc. 7th International Computer Science Symposium in Russia (CSR). DOI

Autres contributions

Cours enseignés ou supervisés à l'UdeS

  • IFT503 - Théorie du calcul. (2024-2026). (3CR).
  • IFT711 - Théorie du calcul. (2024-2026). (3CR).
  • IFT436 - Algorithmes et structures de données. (2023-2025). (3CR).
  • IFT769 - Sujets choisis en informatique théorique. (2025). (3CR).
  • IGL502 - Techniques de vérification et de validation. (2023-2025). (3CR).
  • IGL752 - Techniques de vérification et de validation. (2023-2025). (3CR).
  • IFT209 - Programmation système. (2024). (3CR).