Michael Blondin

TUM

I am a postdoctoral researcher at the Chair for Foundations of Software Reliability and Theoretical Computer Science of the Technical University of Munich. I work on theoretical and practical aspects of formal verification. My interests include model checking of concurrent and distributed systems, verification tools, computational complexity theory, automata theory and arithmetic theories. My recent work deals with verification problems for systems having infinitely many configurations, such as Petri nets, vector addition systems, population protocols and well-structured transition systems.

Publications

Journals (peer-reviewed)

Conferences (peer-reviewed)

Theses

Tools

  • QCover: an efficient coverability verifier for discrete and continuous Petri nets.

    QCover is a Python 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 TACAS 2016 and TOCL 2017 papers.

  • Peregrine: a tool for the verification of population protocols.

    Peregrine allows to test whether a given population protocol is well-specified and whether it computes a given predicate. Unlike other verification tools for population protocols, Peregrine performs verification over all of the infinitely many initial configurations. At the moment, the tool supports silent protocols, i.e., protocols whose executions eventually stabilize to a terminal configuration. Peregrine is implemented in Haskell and makes use of the SMT solver Z3. More details can be found in our PODC 2017 paper.

Talks

Résumé

Positions and education

Sept. 2016 –
Present
Postdoctoral researcher in computer science
Technische Universität München, 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
Sept. 2007 –
Dec. 2009
Bachelor's (B.Sc.) in computer science
Université de Montréal, Canada
Sept. 2004 –
June 2007
College diploma (DEC) in computer science
Collège Lionel-Groulx, Canada

Awards

May 2017 –
Present
Postdoctoral research fellowship
FRQNT
Winner 2015 Teaching assistant excellence award
Université de Montréal
Jan. 2015 –
June 2016
Frontenac mobility scholarship
FRQNT, MAEDI & 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. 2016 –
Present
Teaching assistant
Technische Universität München
Sep. 2008 –
Dec. 2015
Teaching assistant
Université de Montréal
Jan. 2011 –
Mar. 2011
Lecturer
Université de Montréal

Other professional activities

May 2009 –
Aug. 2009
Research assistant
Theoretical and quantum computer science laboratory
Université de Montréal
Feb. 2007 –
May 2007
Programmer-analyst (intern)
Memberworks Canada

Reviewing

Journals International Journal of Foundations of Computer Science (IJFCS)
Conferences CONCUR, CSR, DCFS, DLT × 2, FSTTCS, ICALP, LICS × 2, MFCS, RP × 2, SOFSEM, STACS

Extra-curricular activities

June 2008 –
Oct. 2012
Computer science and operations research students' association (AÉDIROUM)
Université de Montréal
  • External vice-president (Sep. 2011 – Oct. 2012)
  • President (May 2010 – Sep. 2011)
  • Internal vice-president (May 2009 – Sep. 2010)
  • Student life coordinator (Jan. 2009 – Jan. 2010)
  • Treasurer (June 2008 – May 2009)
Nov. 2010 –
Apr. 2011
Students' associations' federation (FAÉCUM)
Université de Montréal
  • Administrator
  • Member of the grant allocation committee
Mar. 2009 Computer Science Games
Team Université de Montréal
  • First place in "Theory of computation and algorithmic"
  • Member of the winning team

Contact