Michael Blondin
Je suis professeur adjoint au
Département
d'informatique de
l'Université
de Sherbrooke. Ma recherche se situe à l'intersection des méthodes
formelles et
de l'informatique
théorique. J'étudie les fondements de la
vérification
formelle dans le but de permettre un
développement plus fiable de logiciels et de
systèmes informatiques. Mes intérêts
incluent
le model
checking de
systèmes concurrents
et distribués,
les outils de vérification,
la théorie
de la complexité,
la théorie
des automates et
les théories
arithmétiques.
Avant de me joindre à l'Université de Sherbrooke, j'ai obtenu un doctorat en cotutelle de l'ENS
Paris-Saclay et de l'Université
de Montréal, et j'ai également travaillé comme chercheur postdoctoral à l'Université technique de Munich.
Publications
Revues (évaluées par les pairs)
- Michael Blondin, Alain Finkel et Pierre McKenzie. Handling Infinitely Branching Well-structured Transition Systems. Information and Computation, vol. 258, pp. 28–49, 2018.
- Michael Blondin, Alain Finkel, Christoph Haase et 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 et Pierre McKenzie. Well Behaved Transition Systems. Logical Methods in Computer Science (LMCS), vol. 13, no. 3, 2017.
- Michael Blondin, Andreas Krebs et Pierre McKenzie. The Complexity of Intersecting Finite Automata Having Few Final States. Computational Complexity, vol. 25, no. 4, pp. 775–814, 2016.
Contributions invitées
- Michael Blondin, Javier Esparza, Stefan Jaax et Antonín Kučera. Black Ninjas in the Dark: Formal Analysis of Population Protocols. LICS 2018.
Conférences (évaluées par les pairs)
- Michael Blondin, Christoph Haase et Filip Mazowiecki. Affine Extensions of Integer Vector Addition Systems with States. CONCUR 2018 (to appear).
- Michael Blondin, Javier Esparza et Antonín Kučera. Automatic Analysis of Expected Termination Time for Population Protocols. CONCUR 2018 (to appear).
- Michael Blondin, Javier Esparza et Stefan Jaax. Peregrine: A Tool for the Analysis of Population Protocols. CAV 2018.
- Michael Blondin, Javier Esparza et Stefan Jaax. Large Flocks of Small Birds: On the Minimal Size of Population Protocols. STACS 2018.
- Michael Blondin, Alain Finkel et Jean Goubault-Larrecq. Forward Analysis for WSTS, Part III: Karp-Miller Trees. FSTTCS 2017.
- Michael Blondin, Javier Esparza, Stefan Jaax et Philipp J. Meyer. Towards Efficient Verification of Population Protocols. PODC 2017.
- Michael Blondin et Christoph Haase. Logics for Continuous Reachability in Petri Nets and Vector Addition Systems with States. LICS 2017.
- Michael Blondin, Alain Finkel, Christoph Haase et Serge Haddad. Approaching the Coverability Problem Continuously. TACAS 2016.
- Michael Blondin, Alain Finkel, Stefan Göller, Christoph Haase et Pierre McKenzie. Reachability in Two-Dimensional Vector Addition Systems with States is PSPACE-complete. LICS 2015.
- Michael
Blondin, Alain Finkel et Pierre McKenzie. Handling
Infinitely Branching WSTS. ICALP
2014.
- Michael Blondin et Pierre McKenzie. The Complexity of Intersecting Finite Automata Having Few Final States. CSR 2012.
Thèses et mémoires
- Algorithmique et complexité des systèmes à compteurs. Thèse de doctorat (Ph.D.), ENS Cachan – Université Paris-Saclay et Université de Montréal, 2016.
- Complexité raffinée du problème d'intersection d'automates. Mémoire de maîtrise (M.Sc.), Université de Montréal, 2012.
- Complexité du problème d'intersection d'automates. Mémoire de baccalauréat honor (B.Sc.), Université de Montréal, 2009.
Outils
- Peregrine: un outil pour l'analyse
formelle des protocoles de populations.
Peregrine est un outil pour l'analyse et la vérification paramétrée des protocoles de populations, un modèle de calcul distribué dans lequel des agents anonymes et mobiles interagissent de façon stochastique afin d'accomplir une tâche commune. Les fonctionnalités de Peregrine incluent la simulation manuelle pas-à-pas; l'échantillonnage automatique; la génération de statistiques sur le temps de convergence; la détection d'exécutions erronées via simulation; et la vérification formelle de correction. Les quatre premières fonctionnalités sont supportées pour tous les protocoles, et la vérification est supportée pour les protocoles silencieux, une grande sous-classe de protocoles de populations. Pour plus de détails, voir les articles CAV 2018 et PODC 2017.
- QCover: un outil efficace pour la
vérification des réseaux de Petri continus et
discrets.
QCover est une implémentation d'une procédure qui permet de décider le problème de couverture pour les réseaux de Petri. Cette procédure utilise l'accessibilité dans les réseaux de Petri continus comme critère d'élagage dans le cadre d'un algorithme d'exploration arrière. Le cœur de l'approche repose sur un traduction logique de l'accessibilité continue dans le solveur SMT Z3. QCover peut également être utilisé pour décider l'accessibilité et la couverture dans les réseaux de Petri continus. Pour plus de détails, voir les articles TOCL 2017 et TACAS 2016.
Présentations
- – Affine Extensions of Integer Vector Addition Systems
with States
– Automatic Analysis of Expected Termination Time for Population Protocols
CONCUR, 7 septembre 2018, Pékin, Chine. - Formal Verification of
Population Protocols
Autobóz: workcamp on automata, logic and games theory, 18 juillet 2018, Gèdre, France. - Formal
Analysis of Population Protocols
Dagstuhl Seminar 18211 (Formal Methods and Fault-Tolerant Distributed Computing: Forging an Alliance), 24 mai 2018, Wadern, Allemagne. - Automatic
Analysis of Expected Termination Time for Population
Protocols
Séminaire du LSV, ENS Paris-Saclay, 15 mai 2018, Cachan, France. - On the State
Complexity of Population
Protocols
Verification Seminar, University of Oxford, 29 mars 2018, Oxford, Royaume-Uni. -
– 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, 16 mars 2018, Eichstätt, Allemagne. - Vérification automatique
de systèmes
infinis
Université de Sherbrooke, Département d'informatique, 6 octobre 2017, Sherbrooke, Canada. - Reachability in VASS with Two
Counters
Autobóz: workcamp on automata, logic and games theory, 22 juillet 2017, Koninki, Pologne. - On Tools for
Coverability
Gregynog 71717: Workshop on Vector Addition Systems, 6 juillet 2017, Tregynon, Royaume-Uni. - Logics for Continuous
Reachability in Petri Nets and Vector Addition Systems with
States
LICS, 20 juin 2017, Reykjavik, Islande. - Towards Efficient
Verification of Population
Protocols
Verification Seminar, University of Oxford, 24 mai 2017, Oxford, Royaume-Uni. - The Logical View on
Continuous Petri Nets
PUMA Workshop, 13 octobre 2016, San Martino in Passiria, Italie. - Approaching the
Coverability Problem
Continuously
PUMA Seminar, Université technique de Munich, 11 mai 2016, Garching, Allemagne. - Approaching the
Coverability Problem
Continuously
TACAS, 6 juillet 2016, Eindhoven, Pays-Bas. - Reachability in
Two-Dimensional Vector Addition Systems with States is
PSPACE-complete
LICS, 6 juillet 2015, Kyoto, Japon. - Reachability in
Two-Dimensional Vector Addition Systems with States is
PSPACE-complete
Journées annuelles du GT-Verif, 15 juin 2015, Créteil, France. - Reachability in
Two-Dimensional Vector Addition Systems with
States
Automata theory group seminar, Université de Varsovie, 18 mai 2015, Varsovie, Pologne. - Reachability
in continuous vector addition systems: from
theory to practice
Séminaire INFINI, LSV, ENS Cachan, 13 mai 2015, Cachan, France. - Accessibilité dans les
systèmes d’addition de vecteurs à deux
compteurs
LITQ Seminar, Université de Montréal, 14 février 2015, Montréal, Canada. - Handling Infinite
Branching WSTS
ICALP, 8 juillet 2014, Copenhague, Danemark. - Handling Infinite
Branching WSTS
Journées Recherche DigiCosme, 2 juillet 2014, Orsay, France. - Handling Infinite
Branching WSTS
Journées annuelles du GT-Verif, 16 juin 2014, Paris, France. - Handling
Infinite Branching WSTS
Dagstuhl Seminar 14141 (Reachability Problems for Infinite-State Systems), 31 mars 2014, Wadern, Allemagne. - Handling
Infinite Branching WSTS
Séminaire ReacHard, LaBRI, Université de Bordeaux, 6 janvier 2014, Talence, France. - The Complexity
of Intersecting Finite Automata Having Few Final
States
Séminaire INFINI, LSV, ENS Cachan, 31 octobre 2013, Cachan, France. - The
Complexity of Intersecting Finite Automata Having Few
Final States
CSR, 7 juillet 2012, Nijni Novgorod, Russie.
Curriculum vitæ
Postes |
|
|---|---|
| Sep. 2018 – Présent |
Professeur adjoint Département d'informatique Université de Sherbrooke, Canada |
| Sep. 2016 – Juil. 2018 |
Chercheur postdoctoral Chair for foundations of software reliability and theoretical computer science Université technique de Munich, Allemagne |
Éducation |
|
| Avr. 2013 – Juin 2016 |
Doctorat (Ph.D.) en informatique (cotutelle) ENS Cachan – Université Paris-Saclay, France |
| Jan. 2012 – Juin 2016 |
Doctorat (Ph.D.) en informatique (cotutelle) Université de Montréal, Canada |
| Jan. 2010 – Jan. 2012 |
Maîtrise (M.Sc.) en informatique Université de Montréal, Canada |
| Sep. 2007 – Déc. 2009 |
Baccalauréat (B.Sc.) en informatique Université de Montréal, Canada |
| Sep. 2004 – Juin 2007 |
Technique (DEC) en informatique de gestion Collège Lionel-Groulx, Canada |
Financement et prix |
|
| Mai 2017 – Juil. 2018 | Bourse de recherche postdoctorale FRQNT |
| Lauréat 2015 | Prix d’excellence aux auxiliaires d’enseignement, Université de Montréal |
| Jan. 2015 – Juin 2016 |
Bourse de mobilité Frontenac FRQNT, MAEDI and MRIF |
| Mai 2013 – Déc. 2014 |
Bourse de doctorat de recherche FRQNT |
| Oct. 2010 – Déc. 2011 |
Bourse de maîtrise de recherche FRQNT |
| Mai 2009 – Août 2009 |
Bourse de recherche de premier cycle CRSNG |
| Sep. 2007 – Déc. 2009 |
Bourse d’excellence à
l’admission DIRO, Université de Montréal |
Enseignement |
|
| Sep. 2018 – Présent |
Professeur Université de Sherbrooke
|
| Sep. 2016 – Juil. 2018 |
Auxiliaire d'enseignement Université technique de Munich |
| Sep. 2008 – Déc. 2015 |
Auxiliaire d'enseignement Université de Montréal
|
| Jan. 2011 – Mars 2011 |
Chargé de cours Université de Montréal
|
Évaluation d'articles |
|
| Revues | ACM Transactions on Embedded Computing Systems (TECS), International Journal of Foundations of Computer Science (IJFCS) |
| Conférences | CONCUR, CSR, DCFS, DISC, DLT × 2, FoSSaCS, FSTTCS, ICALP, LICS × 2, MFCS, RP × 2, SOFSEM, STACS, STOC |