Note ABES Interactive compilation via trustworthy source-to-source transformations Compilation interactive par des transformations source-à-source dignes de confiance Code haute performance Preuve de programme Optimisation source-à-source Compilation Logique de séparation High performance code Software verification Source-to-source optimization Compilation Separation logic 005 Code source (informatique) Calcul intensif (informatique) Les programmeurs sont confrontés à deux facteurs limitants : leur capacité à produire du code sans bogues et la puissance de calcul de leur matériel. L'optimisation manuelle du code peut repousser les limites du matériel, mais elle est chronophage, car elle augmente la taille du code et le risque de bogues.Cette thèse vise à réduire le travail nécessaire pour produire un code optimisé et exempt de bogues. Pour cela, nous avons développé le compilateur interactif OptiTrust qui applique des transformations source-à-source guidées par l'utilisateur.Pour assurer qu'aucune transformation ne crée de bogue, OptiTrust exploite des annotations en logique de séparation initialement fournies par l'utilisateur puis mises à jour automatiquement à chaque étape. Ces annotations peuvent encoder soit une preuve de correction fonctionnelle préservée par les transformations, soit la structure de la mémoire accessible qui permet de vérifier que les transformations préservent la sémantique du code. Programmers are usually facing two limiting factors: their ability to produce code without bugs, and the computing power of their hardware.User-driven code optimization can push the hardware limits further, but it can be time-consuming as it usually increases the code complexity and makes bugs more likely. This thesis aims at reducing the amount of work needed to produce code that is at the same time optimized and exempt from bugs. To achieve this goal, we developed an interactive compiler called OptiTrust, which applies user-guided source-to-source transformations.To guarantee that each transformation does not create a bug, OptiTrust leverages separation logic resource annotations initially written by the user and updated automatically at each step. These annotations can encode either a functional correctness proof, which is preserved through transformations, or the shape of the accessible mutable memory, which can be used to check that transformations preserve code semantics. Electronic Thesis or Dissertation Text en PDF 1468291 https://publication-theses.unistra.fr/public/theses_doctorat/2025/BERTHOLON_Guillaume_2025_ED269.pdf http://www.theses.fr/2025STRAD013/abes https://theses.hal.science/tel-05302456 https://theses.hal.science/tel-05302456 https://theses.hal.science/tel-05302456 https://theses.hal.science/tel-05302456 Bertholon Guillaume 1997-02-05 FR 290961572 2508019469U 22220110 4200018 https://theses.fr/2025STRAD013 2025STRAD013 https://doi.org/10.70675/c96ce4b6z259cz4adez8d3azfb9185492a3f 2025-09-22 Informatique Strasbourg 131056549 Doctorat Docteur es non oui Charguéraud Arthur MADS_DIRECTEUR_DE_THESE_1 2700 150248792 Magaud Nicolas MADS_PRESIDENT_DU_JURY 077385969 Keller Chantal MADS_MEMBRE_DU_JURY_1 176956875 Dagand Pierre-Evariste MADS_MEMBRE_DU_JURY_2 253134765 Monniaux David MADS_RAPPORTEUR_1 070681600 Merz Stephan MADS_RAPPORTEUR_2 120558513 École doctorale Mathématiques, sciences de l'information et de l'ingénieur (Strasbourg ; 1997-....) MADS_ECOLE_DOCTORALE_1 269 156504863 Laboratoire des sciences de l'ingénieur, de l'informatique et de l'imagerie (Strasbourg ; 2013-....) MADS_PARTENAIRE_DE_RECHERCHE_1 260728 176969721 ddc:004 Charguéraud Arthur Magaud Nicolas Keller Chantal Dagand Pierre-Evariste Monniaux David Merz Stephan École doctorale Mathématiques, sciences de l'information et de l'ingénieur (Strasbourg ; 1997-....) Laboratoire des sciences de l'ingénieur, de l'informatique et de l'imagerie (Strasbourg ; 2013-....) PDF 1468291