Læ candidat·e prendra part au développement de l’analyseur formel PyRAT, développé au sein du laboratoire. Cet analyseur à l’état de l’art de la vérification formelle de réseaux de neurones est le siège d’autant de thématiques de recherches que d’applications industrielles pour le laboratoire. À ce titre, læ candidat·e évoluera à la frontière entre les mondes de la recherche scientifique et du développement logiciel industriel. Les missions de læ candidat·e sont les suivantes :

· Étude active et restitution de l’état de l’art de la vérification formelle de logicielle, en particulier celle portant sur les programmes d’Intelligence Artificielle, et les explications de programmes d’Intelligence Artificielle.
· Participation aux discussions et décisions scientifiques et techniques sur les améliorations à apporter dans l’analyseur PyRAT. Implémentation de ces améliorations.
· Développement du lien entre la thématique de vérification formelle et celle d’explicabilité formelle. Application et amélioration de PyRAT pour l’explicabilité formelle.
· Participation aux divers projets académiques, européens ou industriels autour de PyRAT et de l’explicabilité formelle et application aux cas d’usages étudiés.
· Rédaction de rapports techniques et/ou de publications scientifiques portant sur l’analyseur formel PyRAT.
· Support au développement de l’analyseur formel PyRAT, notamment par la rédaction de documentation, tutoriels, organisation de sessions de développement communes, relecture de contributions extérieures.
· Participation à des congrès (nationaux et internationaux) pour disséminer les travaux sur l’analyseur PyRAT et l’explicabilité formelle.