Les étudiants qui intègrent IMT Atlantique sont au contact direct d’enseignants-chercheurs reconnus pour leur expertise dans leur domaine. Ils peuvent en plus choisir de suivre durant leur cursus un parcours « excellence par la recherche ». Exemple avec le logiciel Coq au cœur des travaux d’Assia Mahboubi, chargée de recherche INRIA, bourse ERC (European Research Council) Consolidator Grant 2020.
Assia Mahboubi est membre de l’équipe projet Gallinette, équipe mixte Inria, Université de Nantes et IMT Atlantique, qui travaille sur une nouvelle génération d'assistants de preuve (de langages de programmation notamment), avec l'idée directrice que l'expérimentation pratique va de pair avec la recherche fondamentale. Assia vient de recevoir la prestigieuse bourse européenne pour un projet sur la formalisation des résultats mathématiques grâce à des logiciels de vérification appelés assistant de preuve.
" Au coeur du projet d'Assia Mahboubi, le logiciel Coq développé par Inria, permet de démontrer des théorèmes mathématiques et de programmer. Il est fondé sur une correspondance fondamentale qu'on peut résumer par une double équivalence: programmer = démontrer, spécifier = conjecturer, » explique Hervé Grall, enseignant-chercheur au département Automatique, Productique et Informatique d’IMT Atlantique et aussi membre de l’équipe Gallinette.
Préparer les futurs ingénieurs des industries de pointe
Aux élèves d’IMT Atlantique, l’initiation à Coq est proposée dans un double cadre : des cours dans la formation par apprentissage en ingénierie logicielle (FIL) et des projets dans le parcours d'excellence par la recherche, qui peut être choisi dès la première année de la formation d'ingénieurs. « C'est en effet un formidable outil pour l'apprentissage de la logique et de la programmation certifiée : une initiation à l'art de raisonner sans erreur, et à l'art de programmer sans bug," souligne Hervé Grall.
Rémi Douence, autre enseignant-chercheur de l’équipe à IMT Atlantique précise: "Depuis sa création les élèves apprentis ingénieurs de la filière ingénierie logicielle sont sensibilisés aux méthodes formelles pour la qualité logicielle. Depuis l’année scolaire 2019-2020, cette formation intègre une initiation à l’outil Coq qui permet de certifier mécaniquement des logiciels. Cette formation sensibilise les étudiants à une approche rigoureuse du développement logiciel qui commence à faire son apparition dans des industries de pointe et devrait se démocratiser dans les décennies à venir."
Preuve s’il en était encore besoin que se former par et/ou pour la recherche, c’est bien prendre une longueur d’avance … et travailler son employabilité avant même la sortie de l’Ecole !
En savoir plus
Si la graine du chercheur se réveille en vous, les portes des laboratoires vous sont ouvertes durant la formation : en savoir plus sur le parcours d’excellence par la recherche
En savoir plus sur les travaux de recherche et la bourse ERC Consolidator Grant 2020 d’Assia Mahboubi
par Fabienne MILLET-DEHILLERIN
