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 algorithmique dans le but de permettre un développement plus fiable de logiciels et de systèmes informatiques. Mes intérêts incluent la vérification formelle, 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)

Contributions invitées

Conférences (évaluées par les pairs)

Thèses et mémoires

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

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

Contact