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 algorithmic verification with the intended goal of allowing for the development of more reliable software and systems. My interests include formal verification, automata theory, model checking of concurrent and distributed systems, computational complexity theory, logic and verification tools.

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.



Journals (peer-reviewed)

Invited contributions

International conference proceedings (peer-reviewed)



  • 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.

  • 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.

  • 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.


Research team

If you are interested in working under my supervision, please do not hesitate to send me an email.


Jan. 2022 –
Alex Sansfaçon-Buchanan
Master's student (M.Sc.)
Jan. 2022 –
Noé Canva
Master's student (M.Sc.)
Sep. 2021 –
Jan. 2024
François Ladouceur
Master's student (M.Sc.)
Jan. 2020 –
June 2023
Philip Offtermatt
Ph.D. student, Université de Sherbrooke
(coadvised with Filip Mazowiecki at the University of Warsaw)
Summer 2021 Noé Canva
Undergraduate intern
Fall 2020 Alex Sansfaçon-Buchanan
Undergraduate intern
Feb. 2020 –
July 2020
Juliette Fournis d'Albiat
Master's intern (M1) (from the ENS Paris-Saclay)
Sep. 2018 –
Nov. 2018
Stefan Jaax
Ph.D. intern (from the Technical University of Munich)


Oct. 2021 Filip Mazowiecki
Researcher, Max Planck Institute for Software Systems (Saarbrücken)
May 2019 Filip Mazowiecki
Postdoc, Université de Bordeaux
Oct. 2019
Oct. – Nov. 2018
Alain Finkel
Professor, ENS Paris-Saclay

Résumé (short version)


June 2023 –
Associate professor (tenured)
Computer science department
Université de Sherbrooke, Canada
Sep. 2018 –
May 2023
Assistant professor
Computer science department
Université de Sherbrooke, Canada
Sep. 2016 –
July 2018
Postdoctoral fellow
Chair for foundations of software reliability and theoretical computer science
Technical University of Munich, Germany


Apr. 2013 –
June 2016
Ph.D. in computer science (joint)
ENS Cachan – Université Paris-Saclay, France
Jan. 2012 –
June 2016
Ph.D. in computer science (joint)
Université de Montréal, Canada
Jan. 2010 –
Jan. 2012
Master's (M.Sc.) in computer science
Université de Montréal, Canada
Sep. 2007 –
Dec. 2009
Bachelor's (B.Sc.) in honours computer science
Université de Montréal, Canada
Sep. 2004 –
June 2007
College diploma (DEC) in computer science
Collège Lionel-Groulx, Canada

Grants and awards

May 2022 Invited professor, Université de Mons, Belgium  (2 500€)
FNRS (invited by Mickael Randour)
Apr. 2021 –
Mar. 2023
Research support for new academics  (60 000$)
Apr. 2019 –
Mar. 2025
Discovery grant  (150 500$)
May 2019 –
July 2019
Short-term research stays funding: Quebec – Bavaria  (6 500$)
Sep. 2018 –
Mar. 2019
Start-up funds  (17 500$)
May 2017 –
July 2018
Postdoctoral research fellowship  (43 750$)
Winner 2015 Teaching assistant excellence award  (1 000$)
Université de Montréal
Jan. 2015 –
June 2016
Frontenac mobility scholarship  (8 514$)
May 2013 –
Dec. 2014
Doctoral research scholarship  (33 333$)
Oct. 2010 –
Dec. 2011
Master's research scholarship  (25 000$)
May 2009 –
Aug. 2009
Undergraduate student research award  (5 675$)
Sep. 2007 –
Dec. 2009
Academic excellence entry scholarship  (6 000$)
Computer science department, Université de Montréal


Sep. 2018 –
Université de Sherbrooke
Sep. 2016 –
July 2018
Teaching assistant
Technical University of Munich
Sep. 2008 –
Dec. 2015
Teaching assistant
Université de Montréal
Jan. 2011 –
Mar. 2011
Université de Montréal


External committees
  • Program committee: MFCS 2024, CONCUR 2023, SOFSEM 2023, ICALP 2021, MFCS 2020
  • Evaluation committee, doctoral research scholarships (ICT), FRQNT (W22)
  • Evaluation committee, merit scholarship program for foreign students, FRQNT (W20, W19)