SCD-Universite de Rennes 1 Formal verification of weak topological orderings and dataflow analysis Vérification formelle de tris topologiques faibles et analyse flots de données vérification formelleanalyse statiqueRocqcompilation optimisante formal verificationstatic analysisRocqcompiler optimizations Logiciels -- Vérification Compilation (informatique) 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. 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. Electronic Thesis or DissertationText en application/pdf1 : 4218 Kohttps://ged.univ-rennes1.fr/nuxeo/site/esupversions/a779f69f-172b-4144-a260-e994a8640676 La Spina Sophia Sophia 2000-10-09 FR 297659898 sophia.laspina@protonmail.com 2025URENS108 http://www.theses.fr/2025URENS108 2025-12-16 Informatique Université de Rennesthesis.degree.grantor_1 26693823X Doctorat non ouiBlazySandrineintervenant_1153042567DemangeDelphineintervenant_2174231989BaeldeDavidintervenant_3201647249BlazySandrineintervenant_1153042567DemangeDelphineintervenant_2174231989KellerChantalintervenant_4176956875MinéAntoineintervenant_5111391636FilliâtreJean-Christopheintervenant_615500395X MATISSEecoleDoctorale_1 267602553 IRISA partenaireRecherche_1 026386909 ddc:004 BlazySandrineDemangeDelphineBaeldeDavidKellerChantalMinéAntoineFilliâtreJean-ChristopheUniversité de RennesMATISSE IRISA ASCII PDF 4319684