Michael Blondin

I am an assistant professor of computer science at the Université de Sherbrooke. 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, verification tools, computational complexity theory, automata theory and arithmetic theories.

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 researcher at the Technical University of Munich.

Publications

Journals (peer-reviewed)

Invited contributions

Conferences (peer-reviewed)

Theses

Tools

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

Talks

Résumé

Positions

Sep. 2018 –
Present
Assistant professor
Computer science department
Université de Sherbrooke, Canada
Sep. 2016 –
July 2018
Postdoctoral researcher
Chair for foundations of software reliability and theoretical computer science
Technical University of Munich, Germany

Education

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 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 2017 –
July 2018
Postdoctoral research fellowship
FRQNT
Winner 2015 Teaching assistant excellence award
Université de Montréal
Jan. 2015 –
June 2016
Frontenac mobility scholarship
FRQNT, MAEDI and MRIF
May 2013 –
Dec. 2014
Doctoral research scholarship
FRQNT
Oct. 2010 –
Dec. 2011
Master's research scholarship
FRQNT
Lists 2009 and 2010 Faculty of arts and sciences dean's list
Université de Montréal
May 2009 –
Aug. 2009
Undergraduate student research award
NSERC
Sep. 2007 –
Dec. 2009
Academic excellence entry scholarship
Computer science department, Université de Montréal

Teaching

Sep. 2018 –
Present
Professor
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
Lecturer
Université de Montréal

Reviewing

Journals ACM Transactions on Embedded Computing Systems (TECS), International Journal of Foundations of Computer Science (IJFCS)
Conferences CONCUR, CSR, DCFS, DISC, DLT × 2, FoSSaCS, FSTTCS, ICALP, LICS × 2, MFCS, RP × 2, SOFSEM, STACS, STOC

Contact