| Imprimer |
| Formal verification of weak topological orderings and dataflow analysis (Vérification formelle de tris topologiques faibles et analyse flots de données) La Spina, Sophia - (2025-12-16) / Université de Rennes Formal verification of weak topological orderings and dataflow analysis
| |||
Langue : Anglais Directeur(s) de thèse: Blazy, Sandrine; Demange, Delphine Discipline : Informatique Laboratoire : IRISA Ecole Doctorale : MATISSE Classification : Informatique Mots-clés : vérification formelle, analyse statique, Rocq, compilation optimisante
| |||
Résumé : L'analyse flots de données est une technique d'analyse statique qui détermine des informations sur la propagation des données lors de l'exécution d'un programme informatique, sans exécuter le programme. Ces informations peuvent être notamment utilisées pour optimiser le programme lors de sa compilation. Réaliser une analyse flots de données consiste en général à résoudre un système d'équations. En dehors des méthodes traditionnelles utilisées pour résoudre de tels systèmes, d'autres techniques ont été développées. L'une d'entre elles, qui a été proposée par Bourdoncle en 1993, consiste à pré-calculer une stratégie de résolution de manière à résoudre ensuite le système plus efficacement. Cette thèse vise à développer des solveurs formellement vérifiés, qui se basent sur cette technique de résolution. Premièrement, nous proposons une formalisation rigoureuse de la notion de tri topologique faible (WTO) qui permet de représenter la stratégie pré-calculée. Ensuite, nous implémentons et vérifions formellement avec l'assistant de preuve Rocq deux variantes de résolution proposées par Bourdoncle, appelées stratégies itérative et récursive, ainsi que l'algorithme le plus utilisé pour calculer un WTO. Notre développement est entièrement intégré au compilateur formellement vérifié CompCert. Enfin, nous évaluons expérimentalement nos implémentations, en les comparant aux solveurs de CompCert et à une implémentation non vérifiée du calcul du WTO. Abstract : Dataflow analysis is a static analysis technique that determines information on the propagation of data throughout the execution of a computer program, without actually executing the program. This information can notably be used to optimize the program at compile-time. Performing dataflow analysis usually consists in solving a system of equations. Besides the traditional methods used to solve such systems, other techniques have been developed in the static analysis community. One of them, proposed by Bourdoncle in 1993, consists in pre-computing a solving strategy in order to solve the system more efficiently. This thesis aims at the development of formally verified dataflow solvers that are based on this solving technique. First, we provide a rigorous formalization for the notion of Weak Topological Ordering (WTO), which captures the pre-computed solving strategy. Then, we implement and formally verify in the Rocq proof assistant two flavors of WTO-based solving strategies introduced by Bourdoncle, known as the iterative and the recursive strategy, along with the most commonly used algorithm to compute a WTO. Our development is entirely integrated inside the formally verified compiler CompCert. Finally, we evaluate experimentally our implementations, comparing them to CompCert's dataflow solvers and to an untrusted computation of the WTO. | |||