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 formal
verification with the intended goal of
allowing for the development of more reliable
software and systems. My interests
include 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)
- Michael Blondin, Alain Finkel and Pierre McKenzie. Handling Infinitely Branching Well-structured Transition Systems. Information and Computation, vol. 258, pp. 28–49, 2018.
- Michael Blondin, Alain Finkel, Christoph Haase and Serge Haddad. The Logical View on Continuous Petri Nets. ACM Transactions on Computational Logic (TOCL), vol. 18, no. 3, pp. 24:1–24:28, 2017.
- Michael Blondin, Alain Finkel and Pierre McKenzie. Well Behaved Transition Systems. Logical Methods in Computer Science (LMCS), vol. 13, no. 3, 2017.
- Michael Blondin, Andreas Krebs and Pierre McKenzie. The Complexity of Intersecting Finite Automata Having Few Final States. Computational Complexity, vol. 25, no. 4, pp. 775–814, 2016.
Invited contributions
- Michael Blondin, Javier Esparza, Stefan Jaax and Antonín Kučera. Black Ninjas in the Dark: Formal Analysis of Population Protocols. LICS 2018.
Conferences (peer-reviewed)
- Michael Blondin, Christoph Haase and Filip Mazowiecki. Affine Extensions of Integer Vector Addition Systems with States. CONCUR 2018 (to appear).
- Michael Blondin, Javier Esparza and Antonín Kučera. Automatic Analysis of Expected Termination Time for Population Protocols. CONCUR 2018 (to appear).
- Michael Blondin, Javier Esparza and Stefan Jaax. Peregrine: A Tool for the Analysis of Population Protocols. CAV 2018.
- Michael Blondin, Javier Esparza and Stefan Jaax. Large Flocks of Small Birds: On the Minimal Size of Population Protocols. STACS 2018.
- Michael Blondin, Alain Finkel and Jean Goubault-Larrecq. Forward Analysis for WSTS, Part III: Karp-Miller Trees. FSTTCS 2017.
- Michael Blondin, Javier Esparza, Stefan Jaax and Philipp J. Meyer. Towards Efficient Verification of Population Protocols. PODC 2017.
- Michael Blondin and Christoph Haase. Logics for Continuous Reachability in Petri Nets and Vector Addition Systems with States. LICS 2017.
- Michael Blondin, Alain Finkel, Christoph Haase and Serge Haddad. Approaching the Coverability Problem Continuously. TACAS 2016.
- Michael Blondin, Alain Finkel, Stefan Göller, Christoph Haase and Pierre McKenzie. Reachability in Two-Dimensional Vector Addition Systems with States is PSPACE-complete. LICS 2015.
- Michael Blondin, Alain Finkel and Pierre McKenzie. Handling Infinitely Branching WSTS. ICALP 2014.
- Michael Blondin and Pierre McKenzie. The Complexity of Intersecting Finite Automata Having Few Final States. CSR 2012.
Theses
- Algorithmics and complexity of counter machines. Ph.D. thesis, ENS Cachan – Université Paris-Saclay and Université de Montréal, 2016.
- Complexité raffinée du problème d'intersection d'automates. M.Sc. thesis, Université de Montréal, 2012.
- Complexité du problème d'intersection d'automates. B.Sc. honour thesis, Université de Montréal, 2009.
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
- – Affine Extensions of Integer Vector Addition Systems
with States
– Automatic Analysis of Expected Termination Time for Population Protocols
CONCUR, September 7, 2018, Beijing, China. - Formal Verification of
Population Protocols
Autobóz: workcamp on automata, logic and games theory, July 18, 2018, Gèdre, France. - Formal
Analysis of Population Protocols
Dagstuhl Seminar 18211 (Formal Methods and Fault-Tolerant Distributed Computing: Forging an Alliance), May 24, 2018, Wadern, Germany. - Automatic
Analysis of Expected Termination Time for Population
Protocols
LSV Seminar, ENS Paris-Saclay, May 15, 2018, Cachan, France. - On the State
Complexity of Population
Protocols
Verification Seminar, University of Oxford, March 29, 2018, Oxford, United Kingdom. -
– On the
Analysis of Population
Protocols
– Logics for Continuous Reachability in Petri Nets and Vector Addition Systems with States
Annual Seminar of the Chair for Foundations of Software Reliability and Theoretical Computer Science, March 16, 2018, Eichstätt, Germany. - Vérification automatique
de systèmes
infinis
Université de Sherbrooke, Computer science department, October 6, 2017, Sherbrooke, Canada. - Reachability in VASS with Two
Counters
Autobóz: workcamp on automata, logic and games theory, July 22, 2017, Koninki, Poland. - On Tools for
Coverability
Gregynog 71717: Workshop on Vector Addition Systems, July 6, 2017, Tregynon, United Kingdom. - Logics for Continuous
Reachability in Petri Nets and Vector Addition Systems with
States
LICS, June 20, 2017, Reykjavík, Iceland. - Towards Efficient
Verification of Population
Protocols
Verification Seminar, University of Oxford, May 24, 2017, Oxford, United Kingdom. - The Logical View on
Continuous Petri Nets
PUMA Workshop, October 13, 2016, San Martino in Passiria, Italy. - Approaching the
Coverability Problem
Continuously
PUMA Seminar, Technical University of Munich, May 11, 2016, Garching, Germany. - Approaching the
Coverability Problem
Continuously
TACAS, July 6, 2016, Eindhoven, Netherlands. - Reachability in
Two-Dimensional Vector Addition Systems with States is
PSPACE-complete
LICS, July 6, 2015, Kyoto, Japan. - Reachability in
Two-Dimensional Vector Addition Systems with States is
PSPACE-complete
GT Verification Annual Days, June 15, 2015, Créteil, France. - Reachability in
Two-Dimensional Vector Addition Systems with
States
Automata theory group seminar, Warsaw University, May 18, 2015, Warsaw, Poland. - Reachability
in continuous vector addition systems: from
theory to practice
INFINI Seminar, LSV, ENS Cachan, May 13, 2015, Cachan, France. - Accessibilité dans les
systèmes d’addition de vecteurs à deux
compteurs
LITQ Seminar, Université de Montréal, February 14, 2015, Montreal, Canada. - Handling Infinite
Branching WSTS
ICALP, July 8, 2014, Copenhagen, Denmark. - Handling Infinite
Branching WSTS
DigiCosme Research Days, July 2, 2014, Orsay, France. - Handling Infinite
Branching WSTS
GT Verification Annual Days, June 16, 2014, Paris, France. - Handling
Infinite Branching WSTS
Dagstuhl Seminar 14141 (Reachability Problems for Infinite-State Systems), March 31, 2014, Wadern, Germany. - Handling Infinite
Branching WSTS
ReacHard Seminar, LaBRI, Université de Bordeaux, January 6, 2014, Talence, France. - The
Complexity of Intersecting Finite Automata Having Few
Final States
INFINI Seminar, LSV, ENS Cachan, October 31, 2013, Cachan, France. - The
Complexity of Intersecting Finite Automata Having Few
Final States
CSR, July 7, 2012, Nizhny Novgorod, Russia.
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 |