Michael Blondin

I am an assistant professor of computer science at the Université de Sherbrooke and a member of its Research group on fundamental computer science (GRIF). My research lies at the intersection of formal methods and theoretical computer science. 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, model checking of concurrent and distributed systems, computational complexity theory, automata 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

Conferences (peer-reviewed)




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


Fall 2020 Alex Sansfaçon-Buchanan
Undergraduate intern, Université de Sherbrooke
Feb. 2020 –
July 2020
Juliette Fournis d'Albiat
Master's intern, ENS Paris-Saclay
Jan. 2020 –
Philip Offtermatt
Ph.D. student, Université de Sherbrooke
(coadvised with Filip Mazowiecki at the Max Planck Institute for Software Systems)
Sep. 2018 –
Nov. 2018
Stefan Jaax
Ph.D. intern, Technical University of Munich


May 2019 Filip Mazowiecki
Postdoc, Université de Bordeaux
Oct. 2019
Oct. – Nov. 2018
Alain Finkel
Professor, ENS Paris-Saclay



Sep. 2018 –
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

Apr. 2019 –
Mar. 2023
Discovery grant  (127 500$)
2019 –
Invited professor, Université de Mons  (2 500€)
FNRS (via Thomas Brihaye and Mickael Randour)
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

Services to the profession

  • Program committee of: ICALP 2021, MFCS 2020
  • Evaluation committee of the merit scholarship program for foreign students, FRQNT (Winter 2020, Winter 2019)
  • Theses: Esaie Kuitche (Ph.D. @ UdeS, Summer 2020), Mehrdad Naserdoust (M.Sc. @ Bishop's U., Winter 2020), Steve Tueno (Ph.D. @ UdeS, Fall 2019), Vincent Fély (M.Sc. @ UdeS, Summer 2019)
  • Predoctoral exams: Corentin Haidon (Fall 2019), Michel-Ange Zamor (Summer 2019)