Sites Inria

Portrait : Pablo Frederico Dobal

Dominique Fidel - 24/11/2014

Federico Dobal : un jeune chercheur très international

A 31 ans, Federico Dobal est un jeune doctorant au parcours international.

Membre de l’équipe projet VeriDis, il concentre aujourd’hui ses travaux de recherche sur les modules arithmétiques du solveur veriT.

Quel a été votre parcours jusqu’ici ?

Je suis argentin et j’ai étudié l’informatique à l’Université Nationale de Rosario. Après ma licence j’ai travaillé pendant deux ans dans une société de conseil puis j’ai repris le chemin des études pour passer un master. J’ai aussi fait un stage d’internship en Finlande, à Åbo Akademi University. En 2012, j’ai appris que l’équipe VeriDis d’Inria ouvrait un poste d’Ingénieur Jeune Diplômé dans le cadre d’une Action de Développement Technologique dédiée à l’amélioration du solveur veriT. Deux arguments m’ont incité à postuler : l’excellente réputation d’Inria et l’envie d’avoir une nouvelle expérience à l’international. Ma candidature a été retenue et à l’automne 2013 le contrat a été reconduit pour une année. 

Alors que j’aurais dû quitter Inria, j’ai pu démarrer une nouvelle expérience au sein de l’institut. En effet, je commence actuellement une thèse en cotutelle par l’Université de Lorraine et le Max-Planck-Institut für Informatik sous la responsabilité conjointe de trois membres de VeriDis : Pascal Fontaine, qui était mon référent scientifique pendant les deux années d’IJD, Thomas Sturm, ainsi que Stephan Merz, le responsable de l’équipe.  Cette thèse est financée conjointement par l'ANR et la Région Lorraine.

Quel est le sujet de votre thèse ?  

Je vais plus particulièrement travailler sur les modules arithmétiques linéaires et non linéaires et sur leurs relations avec les autres modules du démonstrateur. Cela permettra d’améliorer l’efficacité et de valider le bon fonctionnement de certains programmes. Dans ce cadre, je vais servir d’interface entre Inria et les équipes du Max-Planck-Institut afin notamment d’améliorer la résolution des problèmes liés à l’arithmétique. Je serai en quelque sorte chargé de faire la synthèse entre les communautés du calcul symbolique et de la preuve.

Quel regard portez-vous sur vos deux premières années au sein d’Inria ?

J’ai beaucoup appris ! Quand je suis arrivé à Nancy, mon bagage en français se limitait à peu près à « Bonjour » et « Au revoir »… Mais j’ai trouvé une petite équipe très internationale, avec des ressortissants de cinq pays différents, et surtout très accueillante et structurante. Cela m’a aidé à prendre mes marques et à progresser sur le plan de la langue, même si j’ai encore du travail en la matière !  Professionnellement ces deux années ont servi de révélateur : j’étais venu pour participer au développement de la plateforme de test du solveur et de fil en aiguille j’ai pris conscience que je pouvais aller plus loin avec un projet de recherche centré sur veriT. C’est un vrai virage dans ma carrière. Après cette thèse, j’aimerais pouvoir me tourner vers l’enseignement supérieur, en Argentine ou ailleurs.

SMT et veriT
Transports, télécommunications, énergie… De nombreux secteurs d’activité nécessitent des programmes informatiques d’un très haut niveau de fiabilité. Depuis quelques décennies, les techniques de vérification peuvent déléguer une partie de l'analyse à des solveurs SMT (Satisfaisabilité Modulo Théories), très prisés pour leur capacité à combiner un raisonnement logique avec quantificateurs et des procédures de décision spécialisées pour certaines théories (arithmétique, égalité, tableaux…). Développé par l’équipe projet VeriDis (commune au centre de recherche Inria Nancy - Grand Est, au Max-Planck Institut de Saarbrücken et au Loria – CNRS, Inria et Université de Lorraine-) en collaboration avec l'UFRN (Natal, Brésil), veriT est un solveur SMT enopen source, qui se distingue par sa licence particulièrement permissive. Depuis mars 2014, ce logiciel de recherche est au cœur d’un projet ANR-DFG* baptisé SMArT (pour Satisfaisabilité Modulo Arithmétique et Théories) qui vise à repousser les limites des démonstrateurs actuels en investissant davantage le champs de l’arithmétique non linéaire.

* ANR : Agence nationale pour la recherche – DFG : Deutsche Forschungsgemeinschaft

Mots-clés : Algorithme / programmation / logiciels / architecture / preuves / vérification

Haut de page

Suivez Inria tout au long de son 50e anniversaire et au-delà !