Aller au contenu
Trouver un autre spécialiste

Michael Blondin

Professeur, Faculté des sciences
FAC. SCIENCES Informatique

Présentation

Sujet de recherche

Algorithmes, Complexité (Informatique)

Disciplines de recherche

Informatique

Mots-clés

Algorithmique et théorie de la complexité, Langages formels, Logique, Model checking, Systèmes concurrents et distribués, Théorie des automates, Théorie du calcul, Vérification formelle

Intérêts de recherche

Ma recherche se situe à l'intersection des méthodes formelles et de l'informatique théorique. J'étudie les fondements de la vérification algorithmique dans le but de permettre un développement plus fiable de logiciels et de systèmes informatiques.

Recherche clinique

Langues parlées et écrites

Anglais, Français

Diplômes

(2018). (Postdoctorat, ). Technische Universitat Munich.

(2016). (Doctorat, informatique). Ecole Normale Supérieure de Cachan.

(2016). (Doctorat, informatique). Université de Montréal.

(2012). (Maîtrise avec mémoire, informatique). Université de Montréal.

(2009). (Baccalauréat, informatique). Université de Montréal.

Expérience académique

Enseignant-chercheur postdoctoral. (2016-2018). Technische Universitat Munich. Allemagne.

Doctorant. (2013-2016). Centre national de la recherche scientifique. France.

Auxiliaire d'enseignement. (2008-2015). Université de Montréal. Canada.

Prix et distinctions

  • Nominé au prix Inspiration - Qualité de service. Université de Sherbrooke. (Distinction).
  • Prix d’excellence aux auxiliaires d’enseignement. Université de Montréal. (Prix).

Financement

  • Subvention. (Obtenu). Chercheur principal. Tremplin vers la découverte. Conseil de Recherches en Sciences Naturelles et Génie du Canada (CRSNG). 12 500 $. (2019-2021)
  • Subvention. (Terminé). Candidat principal. Fonds de démarrage. Fonds de recherche du Québec - Nature et technologies (FRQNT). 17 500 $. (2018-2019)
  • Bourse de recherche. (Terminé). Candidat principal. Algorithmics and complexity of continuous systems verification (Algorithmique et complexité de la vérification des systèmes continus). Fonds de recherche du Québec - Nature et technologies (FRQNT). Bourse de recherche postdoctorale. 43 750 $. (2017-2018)
  • Bourse d’études. (Terminé). Candidat principal. Bourse de mobilité Frontenac. Fonds de recherche du Québec - Nature et technologies (FRQNT). 8 514 $. (2015-2016)
  • Bourse de recherche. (Terminé). Fonds de recherche du Québec - Nature et technologies (FRQNT). Bourse de maîtrise de recherche. 25 000 $. (2010-2011)
  • Bourse d’études. (Terminé). Université de Montréal. Bourse d'excellence à l’admission. 6 000 $. (2007-2009)
  • Bourse de recherche. (Terminé). Conseil de Recherches en Sciences Naturelles et Génie du Canada (CRSNG). Bourse de recherche de premier cycle. 5 675 $. (2009-2009)
  • Bourse d’études. (Terminé). Candidat principal. Bourse de doctorat de recherche. Fonds de recherche du Québec - Nature et technologies (FRQNT). Bourse de doctorat de recherche. 33 333 $.
  • Subvention. (Obtenu). Chercheur principal. Efficient verification of concurrent and distributed infinite-state systems. Conseil de Recherches en Sciences Naturelles et Génie du Canada (CRSNG). Subvention à la découverte. 115 000 $.
  • Subvention. (Terminé). Chercheur principal. Formal verification methods for the development of reliable dynamic networks (Méthodes de vérification formelle pour le développement de réseaux dynamiques fiables). Fonds de recherche du Québec - Nature et technologies (FRQNT). Financement de courtes missions de recherche: Québec – Bavière. 6 500 $.
  • Bourse de recherche. (Obtenu). Cocandidat. Professeur invité, Université de Mons. Fonds de la Recherche Scientifique (FNRS) (Belgique). Mission scientifique. 2 500 $.

Publications

Articles de revue

  • Michael Blondin, Alain Finkel, Jean Goubault-Larrecq. (2020). Forward Analysis for WSTS, Part III: Karp-Miller Trees. Logical Methods in Computer Science (LMCS) 16 (2), (Article publié).
  • Michael Blondin. (2020). The ABCs of Petri net reachability relaxations. ACM SIGLOG News: verification column 7 (3), (Article sous presse).
  • Michael Blondin, Javier Esparza, Stefan Jaax. (2020). Towards Efficient Verification of Population Protocols. Formal Methods in System Design (FMSD) (Article accepté).
  • (2019). Affine Extensions of Integer Vector Addition Systems with States. Logical Methods in Computer Science (LMCS) (Article soumis).
  • Michael Blondin, Matthias Englert, Alain Finkel, Stefan Göller, Christoph Haase, Ranko Lazić, Pierre McKenzie et Patrick Totzke. (2019). The Reachability Problem for Two-Dimensional Vector Addition Systems with States. Journal of the ACM (Article soumis).
  • Michael Blondin, Alain Finkel and Pierre McKenzie. (2018). Handling Infinitely Branching Well-structured Transition Systems. Information and Computation 258 28–49. (Article publié).
  • Michael Blondin, Alain Finkel, Christoph Haase and Serge Haddad. (2017). The Logical View on Continuous Petri Nets. ACM Transactions on Computational Logic (TOCL) 18 (3), 24:1–24:28. (Article publié).
  • Michael Blondin, Alain Finkel and Pierre McKenzie. (2017). Well Behaved Transition Systems. Logical Methods in Computer Science (LMCS) 13 (3), (Article publié).
  • Michael Blondin, Andreas Krebs and Pierre McKenzie. (2016). The Complexity of Intersecting Finite Automata Having Few Final States. Computational Complexity 25 (4), 775–814. (Article publié).

Ressources en ligne

  • (2018). Peregrine: outil pour l’analyse de protocoles de population. Site Web.
  • (2016). QCover: outil pour la vérification automatique de réseaux de Petri. Site Web.

Articles de conférence

  • Michael Blondin, Christoph Haase, Philip Offtermatt. (2021). Directed Reachability for Infinite-State Systems. 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). (Article soumis).
  • Michael Blondin, Javier Esparza, Martin Helfrich, Antonín Kučera et Philipp J. Meyer. (2020). Checking Qualitative Liveness Properties of Replicated Systems with Stochastic Scheduling. 32nd International Conference on Computer-Aided Verification (CAV).
  • Michael Blondin, Javier Esparza, Blaise Genest, Martin Helfrich, Stefan Jaax. (2020). Succinct Population Protocols for Presburger Arithmetic. 37th International Symposium on Theoretical Aspects of Computer Science (STACS).
  • Michael Blondin et Mikhail Raskin. (2020). The Complexity of Reachability in Affine Vector Addition Systems with States. 35th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS).
  • Michael Blondin, Javier Esparza, Stefan Jaax. (2019). Expressive Power of Broadcast Consensus Protocols. 30th International Conference on Concurrency Theory (CONCUR).
  • Michael Blondin, Christoph Haase and Filip Mazowiecki. (2018). Affine Extensions of Integer Vector Addition Systems with States. International Conference on Concurrency Theory (CONCUR). (Article publié).
  • Michael Blondin, Javier Esparza and Antonín Ku?era. (2018). Automatic Analysis of Expected Termination Time for Population Protocols. International Conference on Concurrency Theory (CONCUR). (Article publié).
  • Michael Blondin, Javier Esparza, Stefan Jaax and Antonín Ku?era. (2018). Black Ninjas in the Dark: Formal Analysis of Population Protocols. Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). (Article publié).
  • Michael Blondin, Javier Esparza and Stefan Jaax. (2018). Large Flocks of Small Birds: On the Minimal Size of Population Protocols. Symposium on Theoretical Aspects of Computer Science (STACS). (Article publié).
  • Michael Blondin, Javier Esparza and Stefan Jaax. (2018). Peregrine: A Tool for the Analysis of Population Protocols. International Conference on Computer Aided Verification (CAV). (Article publié).
  • Michael Blondin, Alain Finkel and Jean Goubault-Larrecq. (2017). Forward Analysis for WSTS, Part III: Karp-Miller Trees. IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS). (Article publié).
  • Michael Blondin and Christoph Haase. (2017). Logics for Continuous Reachability in Petri Nets and Vector Addition Systems with States. Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). (Article publié).
  • Michael Blondin, Javier Esparza, Stefan Jaax and Philipp J. Meyer. (2017). Towards Efficient Verification of Population Protocols. ACM Symposium on Principles of Distributed Computing (PODC). (Article publié).
  • Michael Blondin, Alain Finkel, Christoph Haase and Serge Haddad. (2016). Approaching the Coverability Problem Continuously. International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). (Article publié).
  • Michael Blondin, Alain Finkel, Stefan Göller, Christoph Haase and Pierre McKenzie. (2015). Reachability in Two-Dimensional Vector Addition Systems with States is PSPACE-complete. Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). (Article publié).
  • Michael Blondin, Alain Finkel and Pierre McKenzie. (2014). Handling Infinitely Branching WSTS. International Colloquium on Automata, Languages, and Programming (ICALP). (Article publié).
  • Michael Blondin and Pierre McKenzie. (2012). The Complexity of Intersecting Finite Automata Having Few Final States. International Computer Science Symposium in Russia (CSR). (Article publié).

Autres contributions

Présentations

  • (2020). Automata-based formal verification. Séance de cours invité pour CSC344 – Automata theory à DePaul University (en ligne). États-Unis
  • (2020). Formal analysis of crowd systems [COVID: reportée à 2021]. International Workshop on Synthesis of Complex Parameters (SynCoP). Irlande
  • (2019). Affine Extensions of Integer Vector Addition Systems with States. PaVeS Seminar, Université technique de Munich. Allemagne
  • (2019). Automatic analysis of population protocols. International Workshop on Multi-objective Reasoning in Verification and Synthesis (MoRe). Vancouver, Canada
  • (2019). Machines à compteurs: de la calculabilité à la vérification de programmes. Club mathématique, Université de Sherbrooke. Canada
  • (2018). Affine Extensions of Integer Vector Addition Systems with States. International Conference on Concurrency Theory. Beijing, Chine
  • (2018). Automatic Analysis of Expected Termination Time for Population Protocols. LSV Seminar, ENS Paris-Saclay. Cachan, France
  • (2018). Automatic Analysis of Expected Termination Time for Population Protocols. International Conference on Concurrency Theory. Beijing, Chine
  • (2018). Formal Analysis of Population Protocols. Dagstuhl Seminar 18211 Formal Methods and Fault-Tolerant Distributed Computing: Forging an Alliance. Wadern, Allemagne
  • (2018). Formal Analysis of Population Protocols. Autobóz: workcamp on automata, logic and games theory. Gèdre, France
  • (2018). On the State Complexity of Population Protocols. Verification Seminar, University of Oxford. Oxford, Royaume-Uni
  • (2018). Vérification algorithmique pour le développement de systèmes fiables. Club informatique, Université de Sherbrooke. Canada
  • (2017). Logics for Continuous Reachability in Petri Nets and Vector Addition Systems with States. Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). Reykjavík, Islande
  • (2017). On Tools for Coverability. Gregynog 71717: Workshop on Vector Addition Systems. Tregynon, Royaume-Uni
  • (2017). Reachability in VASS with Two Counters. Autobóz: workcamp on automata, logic and games theory. Koninki, Pologne
  • (2017). The Logical View on Continuous Petri Nets. PUMA (Program and model analysis) Annual Workshop Ludwig Maximilian University of Munich and Technical University of Munich. San Martino in Passiria, Italie
  • (2017). Towards Efficient Verification of Population Protocols. Verification Seminar, University of Oxford. Oxford, Royaume-Uni
  • (2016). Approaching the Coverability Problem Continuously. International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Eindhoven, Pays-Bas
  • (2016). Approaching the Coverability Problem Continuously. PUMA (Program and model analysis) seminar, Ludwig Maximilian University of Munich and Technical University of Munich. Allemagne
  • (2015). Reachability in Two-Dimensional Vector Addition Systems with States. Automata theory group seminar, Warsaw University. Warsaw, Pologne
  • (2015). Reachability in Two-Dimensional Vector Addition Systems with States is PSPACE-complete. Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). Kyoto, Japon
  • (2015). Reachability in Two-Dimensional Vector Addition Systems with States is PSPACE-complete. GT Verification Annual Days. Créteil, France
  • (2014). Handling Infinite Branching WSTS. DigiCosme Research Days. Orsay, France
  • (2014). Handling Infinite Branching WSTS. International Colloquium on Automata, Languages, and Programming (ICALP). Copenhagen, Danemark
  • (2014). Handling Infinite Branching WSTS. Dagstuhl Seminar 14141: Reachability Problems for Infinite-State Systems. Wadern, Allemagne
  • (2014). Handling Infinite Branching WSTS. GT Verification Annual Days. Paris, France
  • (2012). The Complexity of Intersecting Finite Automata Having Few Final States. International Computer Science Symposium in Russia. Nizhny Novgorod, Russie, Fédération de