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.

  • Homepage of Peregrine
  • Source code on GitLab
• 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.

  • Current version on GitHub
  • TACAS 2016 version (37.5 MB)

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é

Contact

• michael.blondinusherbrooke.ca
• (+1) 819 821-8000 ext. 66121

• Michael Blondin
  Département d'informatique
  Université de Sherbrooke
  2500 boulevard de l'Université
  Sherbrooke (Québec), J1K 2R1, Canada

• Office D4-1024-1 (Building D4, 1^st floor)
  Faculté des sciences
  2500 boulevard de l'Université
  Sherbrooke (Québec), Canada

• Design adapted from HTML5 UP