Apprentissage automatique pour l'amélioration de la vérification formelle de code

Frama-C, développé dans notre laboratoire, est une plateforme d'analyse de programmes C qui fournit plusieurs analyseurs collaboratifs sous forme de greffons. Frama-C permet à l'utilisateur d'annoter les programmes C avec des spécifications formelles écrites dans le langage ACSL et de combiner plusieurs de ses analyseurs pour les vérifier, notamment les greffons Eva et WP. Les deux fournissent des techniques hautement paramétrables qui nécessitent une maîtrise fine pour une utilisation efficace. De plus, plusieurs de ces techniques sont plus ou moins basées sur des heuristiques et des stratégies qui sont généralement conçues manuellement. Elles sont souvent sous-optimales, fragiles, et nécessitent des connaissances techniques et des efforts considérables pour être conçues. En tant que telles, elles ne se généralisent pas et ne s'adaptent pas bien à différentes bases de code, et doivent être mises à jour au fil du temps. Le but de cette thèse est d'intégrer des approches d'apprentissage machine aux analyseurs statiques de Frama-C afin d'en améliorer la facilité d'utilisation et la scalabilité. La thèse commencera par étudier quelles heuristiques déjà en place dans Eva ou WP pourraient être apprises automatiquement. Par la suite, le doctorant étudiera les meilleures représentations et les algorithmes d'apprentissage les plus adaptés au traitement de code. Le doctorant proposera et implémentera une chaine d'apprentissage automatique pour les stratégies de vérification de code. En outre, le doctorant intégrera de telles stratégies dans Frama-C et évaluera leurs performances par rapport à celles déjà en place aujourd'hui.