Robin Coutelier, titulaire d'un Master en Ingénieur Civil en Informatique de l’Université de Liège, et aujourd'hui doctorant à la Technische Universität Wien (TU Wien) est le lauréat du prix Paul Gochet de la Fondation de l'Université de Liège. Ce prix lui est attribué pour son travail de fin d'études sur les prouveurs automatiques. Ses recherches portent sur le domaine du raisonnement automatique et, plus précisément, sur la conception de programmes informatiques capables de résoudre des tâches nécessitant un raisonnement logique.
D
ans un monde où l'informatique joue un rôle crucial dans de nombreux domaines, des modèles informatiques à la conception de logiciels, une technologie méconnue mais essentielle émerge : les prouveurs automatiques. Ce sont des programmes informatiques qui sont conçus pour démontrer la validité ou la non-validité d'une formule logique en se basant sur des règles formelles de raisonnement. Par ailleurs, de nombreuses tâches de vérification de programmes se ramènent, in fine, à la vérification de formules logiques. Ainsi, il est possible d'utiliser un prouveur automatique, tel que Vampire, cvc5 ou Z3, pour valider ces formules logiques et, par conséquent, vérifier les programmes. C'est dans ce domaine très pointu que Robin Coutelier a orienté ses recherches.
Titulaire d'un master en Ingénieur Civil en informatique obtenu en 2023 à l'ULiège, Robin Coutelier s'est très tôt découvert une passion pour l'élégance des algorithmes en suivant le cours d'algorithmique et de structures de données dispensé par le Pr. Pascal Fontaine. Il s'est dès lors intéressé de près aux solveurs de satisfaisabilité de formules booléennes, un problème, en apparence très abstrait, qui se révèle avoir un impact considérable en informatique, notamment en lien avec le célèbre problème ouvert P≟NP.
"Le sujet de son travail de fin d'études - Chronological vs. non-chronological backtracking in satisfiability modulo theories - portait sur le backtracking chronologique dans les solveurs SMT (satisfaisabilité modulo théories), explique le Pr. Pascal Fontaine qui a supervisé le TFE. Il y a exploré les techniques récentes de backtracking chronologique au sein du solveur propositionnel intégré dans un solveur satisfaisabilité modulo théorie, en alternative au backtracking non-chronologique traditionnellement utilisé." C'est d'ailleurs pour ce travail que Robin Coutelier s'est vu attribuer le prix Paul Gochet 2024. "Je suis très honoré que le comité d'attribution du prix Paul Gochet m'ai octroyé le prix 2024. Ce prix va permettre de poursuivre mes recherches en collaboration avec l'Université de Liège, sur les prouveurs automatiques et les solveurs SMT", se réjouit Robin Coutelier.
Robin Coutelier est aujourd'hui doctorant à l'Université Technique de Vienne (TU Wien) sous la supervision de la Pr. Laura Kovács. Ses recherches s'inscrivent dans la continuité de ses travaux sur le raisonnement automatique, avec un focus particulier sur le logiciel de preuve Vampire, qui domine les compétitions de prouveurs du premier ordre depuis plusieurs années. Un avenir prometteur donc, en rejoignant ce groupe d’excellence à Vienne, berceau de la logique moderne en Europe.
Consulter le TFE de Robin Coutelier
La fondation Gochet récompense un travail de fin d'étude ou de doctorat dans le domaine de la logique, i.e. la science des méthodes de raisonnement, leur formalisation et leur automatisation. Le récipiendaire devra poursuivre des recherches en logique et justifiera soit d'un cursus antérieur réalisé en tout ou en partie à l'Université de Liège, soit de futures recherches à mener à l'Université de Liège.
En décembre dernier, lors de la soirée des Explort Awards de l'AWEX, deux alumni de notre institution ont été récompensées. Toutes deux sélectionnées pour participer à une mission Explort, elles nous livrent leur retour d’expérience.
Découvrez comment nos chercheurs utilisent l'intelligence artificielle pour détecter des exoplanètes, prévoir la météo, protéger nos cultures ou encore assister les médecins.
Tous les trois scientifiques au sein du GIGA Institute, il reçoivent cette subvention pour leurs projets ambitieux en neurosciences et en oncologie pédiatrique.
