Accéder directement au contenu Accéder directement à la navigation
Thèse

Programmation vérifiée à l'intersection des types dépendants et de l'analyse statique

Résumé : La programmation dirigée par les types ou orientée preuves consiste à écrire et prouver des programmes simultanément. Elle émerge grâce aux langages équipés de types dépendants, et permet une formidable qualité logicielle, au prix de temps passé à écrire des preuves. Inversement, l’analyse statique vise à inférer des propriétés en analysant des programmes existants.Cette thèse étudie la façon dont les systèmes avancés de typage et l’analyse statique peuvent coopérer. Quant à l’analyse statique, nous nous focalisons principalement sur une théorie correcte d’approximation de programmes : l’interprétation abstraite. Notre première contribution démontre l’efficacité de la programmation orientée preuves (avec le langage F*) pour écrire des interpréteurs abstraits formellement vérifiés. De tels interpréteurs existent, mais requièrent une expertise avec les assistants de preuves et en interprétation abstraite, les rendant particulièrement inaccessibles. Notre approche ne nécessite que très peu de preuves manuelles (un ordre de magnitude inférieur en comparaison avec les travaux similaires) : notre implémentation est particulièrement concise et accessible. Nous avons ensuite étudié l’hybridation d’interpréteurs abstraits et de monades de pré-condition la plus faible (WP). Notre approche instrumente des interpréteurs abstraits en des transformeurs de monades de WP. Enfin, nous avons travaillé sur les bénéfices des types dépendants et du système d’effets de F* pour le contrôle de flux d’information (IFC). Nous présentons une librairie permettant de vérifier des politiques d’IFC de manière flexible, entre statique et dynamique.
Type de document :
Thèse
Liste complète des métadonnées

https://tel.archives-ouvertes.fr/tel-03617659
Contributeur : ABES STAR :  Contact
Soumis le : mercredi 23 mars 2022 - 15:52:08
Dernière modification le : vendredi 5 août 2022 - 14:54:52
Archivage à long terme le : : vendredi 24 juin 2022 - 19:43:48

Fichier

2021ENSR0030_FRANCESCHINO_Luca...
Version validée par le jury (STAR)

Identifiants

  • HAL Id : tel-03617659, version 1

Citation

Lucas Franceschino. Programmation vérifiée à l'intersection des types dépendants et de l'analyse statique. Autre [cs.OH]. École normale supérieure de Rennes, 2021. Français. ⟨NNT : 2021ENSR0030⟩. ⟨tel-03617659⟩

Partager

Métriques

Consultations de la notice

91

Téléchargements de fichiers

39