Jasmin Blanchette, de l’équipe Mosel-Veridis, a obtenu une ERC Starting Grant pour son projet Matryoshka portant sur la preuve interactive et les assistants de preuve.
Sur quoi portent précisément vos travaux ?
Mes travaux portent sur la preuve interactive, les assistants de preuve. Lorsqu’on veut utiliser un théorème, on doit le prouver en premier. C’est ce que font les mathématiciens à longueur de journée, mais aussi les informaticiens quand ils veulent vérifier que leurs algorithmes et programmes sont corrects. Les assistants de preuve (par exemple, Coq et Isabelle) sont des logiciels qui aident à développer des preuves mathématiques, pour démontrer de manière très rigoureuse des théorèmes. Mes travaux portent autant sur le développement de ce type de logiciels que sur leur utilisation.
Qu’est-ce qui vous a attiré vers ce domaine de recherche ?
Percer le mystère ! C’est un concours de circonstances qui m’a amené à la preuve interactive : lors de mon bachelor, j’ai eu des cours de preuve mathématique et naïvement je me suis dit qu’un logiciel informatique pourrait remplacer nos preuves faites sur papier et que c’était une idée en or. Ce que je ne savais pas à l’époque, c’est que ce type de logiciels existait déjà ! Lors de mon retour à l’université pour mon master, j’ai rejoint le groupe des méthodes formelles. J’ai alors découvert l’existence les assistants de preuve et ce fut une révélation. Une fois mon master terminé, j’ai cherché un directeur de thèse travaillant dans le domaine de la preuve interactive sans en avoir fait, tout en sachant que ça me plairait et ce fut le cas.
Dans la vie, il faut suivre ses impulsions, plus que ses connaissances ou ses talents ; on est toujours meilleur quand on est motivé !
Quel est l’objectif de la recherche que vous avez proposée à l’ERC ?
Dans le domaine de la preuve informatique, il y a deux communautés qui sont un peu en opposition : les chercheurs qui font de la preuve interactive et ceux qui font de la preuve automatique. Pour moi, cette distinction est plutôt artificielle car on utilise de l’automatique dans l’interactif, et même les outils soi-disant automatiques font appel à l’utilisateur. Avec mon projet d’ERC, je souhaite influencer les deux communautés. À Inria Nancy – Grand Est et Sarrebruck, on a la chance d’avoir des experts dans les deux domaines.
Mon projet s’attache donc à combiner ces deux communautés, en développant la preuve automatique mais appliquée à la preuve interactive. Les outils automatiques sont puissants mais restreints à des logiques peu expressives alors que les assistants de preuve ont des logiques plus riches et sont généralement plus fiables mais sont moins bien automatisés. J’aimerais combiner les atouts des deux types de logiciels, tout en minimisant les défauts.
Je propose une approche par les poupées russes, d’où le nom de Matryoshka. Ce projet est ambitieux mais il a été jugé réalisable, notamment grâce à l’expertise locale sur laquelle je peux compter à Nancy et Sarrebruck.
Quelle est la recette pour décrocher une bourse ERC du premier coup ?
Il faut convaincre différentes personnes, qu’elles soient expertes du domaine ou non, que le projet est cohérent dans sa mise en œuvre et que toutes les étapes énoncées participent de son avancée. Quand on candidate à une ERC, il faut penser communication, expliquer clairement le projet, avoir une police de caractères agréable et des diagrammes utiles, et donc s’attacher autant à la forme du projet qu’au fond. Chaque mot, comme une rime dans un poème, doit conduire vers l’objectif du projet le plus naturellement possible. Il faut pour cela correctement identifier le problème principal et aboutir à un processus qui le résolve. Le projet doit être compréhensible sans effort de la part du lecteur. Chez Inria, on a la chance d’être très bien encadré. J’ai eu l’aide de beaucoup de collègues, que je remercie vivement. Je tiens à rendre tout particulièrement hommage à mon accompagnateur, Jean-Pierre Banâtre, pour ses retours très francs.
Et puis, il faut croire en son projet et en soi : seuls 10 % des candidats obtiennent une ERC. Je me suis dit qu’il fallait que je propose un projet clairement meilleur que les autres ; j’ai donc étudié des projets antérieurs et je me suis assuré que mon texte était plus convaincant. Le projet m’est venu en tête plusieurs mois avant sa rédaction. Il était un peu comme la statue que perçoit un sculpteur dans un bloc de marbre. Les premières idées ont émergé dans un restaurant alors que j’attendais un ami. J’ai encore la nappe sur laquelle elles sont écrites…
Comment allez-vous utiliser ce financement ?
Le budget alloué me permettra de monter une équipe, d’embaucher des doctorants, des ingénieurs, de financer des déplacements à des conférences ou encore d’inviter des chercheurs. Ce sera une équipe distribuée entre Nancy et Sarrebruck pour permettre plus d’échange et de coopération : une équipe qui me ressemble !
Plus d’informations sur le European Research Council
Mosel-VeriDis est une équipe-projet commune à Inria, au CNRS, à l’Université de Lorraine et au Max-Planck-Institut für Informatik.
Biographie express
- 1978 : naissance
- 1997-2000 : bachelor informatique à l’Université de Sherbrooke (Canada)
- 2000-2008 : développeur de logiciels chez Trolltech, une société norvégienne (maintenant appelée The Qt Company)
- 2006-2008 : master informatique à l’Université d’Oslo
- 2008-2012 : doctorat à la Technische Universität München(Munich)
- 2012-2014 : postdoc à la Technische Universität München
- Janvier 2015 : researcher (starting research scientist ) chez Inria Nancy – Grand Est et guest researcher au Max-Planck-Institut für Informatik à Sarrebruck
Chloé Beri, Inria Nancy - Grand Est