Michael Blondin


I work as a postdoctoral researcher at the Chair for Foundations of Software Reliability and Theoretical Computer Science of the Technical University of Munich. I am mainly interested in the verification of concurrent systems and softwares, model checking, computational complexity theory, automata theory, formal languages and logic. My recent work deals with reachability problems in infinite state systems such as Petri nets, vector addition systems and well-structured transition systems.


Journal publications (peer-reviewed)

Conference publications (peer-reviewed)



  • 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 that is based on applying reachability in continuous Petri nets as a pruning criterion inside a backward-coverability framework. The heart of the approach is a sophisticated encoding of reachability in continuous Petri nets into SMT which then enables QCover to use the SMT solver Z3 in order to decide such reachability problems. QCover can also be used to decide reachability and coverability in continuous Petri nets. More details can be found in our TACAS'16 paper and our expanded journal submission.

    QCover is available for the sole purpose of its evaluation and testing. QCover will soon be officially released under an open-source license.


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


Winner 2015 Teaching assistant excellence award
Université de Montréal
Jan. 2015 – June 2016 Frontenac mobility scholarship
May 2013 – Dec. 2014 Doctoral research scholarship
Oct. 2010 – Dec. 2011 Master's research scholarship
Lists 2009 and 2010 Faculty of arts and sciences dean's list
Université de Montréal
May 2009 – Aug. 2009 Undergraduate student research award
Sep. 2007 – Dec. 2009 Academic excellence entry scholarship
Computer science department, Université de Montréal


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
  • ASP.NET programming (Winter 2011)

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

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 & algorithmic"
  • Member of the winning team


  • blondinin.tum.de
  • +49 89 289 17229
  • Michael Blondin
    Institut für Informatik (I7)
    Technische Universität München
    Boltzmannstraße 3
    85748, Garching bei München, Germany

  • Math and Computer Science Building
    Office 03.11.059 (3rd floor, block 11)
    Boltzmannstraße 3
    85748, Garching bei München, Germany