Compilation interactive par des transformations source-à-source dignes de confiance
Langue Anglais
Accéder au document

Ce document est protégé en vertu du Code de la Propriété Intellectuelle.

Modalités de diffusion de la thèse :
  • Thèse consultable sur internet, en texte intégral.
  • Thèse avec 2 versions : seule la version intégrale est proposée ; sur authentification (communication intranet).
 
Auteur : Bertholon, Guillaume
Date de soutenance : 22-09-2025

Directeur(s) de thèse : Charguéraud, Arthur

Président : Magaud, Nicolas
Rapporteur(s) : Monniaux, David - Merz, Stephan
Membre(s) du jury : Keller, Chantal - Dagand, Pierre-Evariste

Établissement de soutenance : Strasbourg
Laboratoire : Laboratoire des sciences de l'ingénieur, de l'informatique et de l'imagerie (Strasbourg ; 2013-....)
École doctorale : École doctorale Mathématiques, sciences de l'information et de l'ingénieur (Strasbourg ; 1997-....)
 
Discipline : Informatique
Classification : Informatique

Mots-clés libres : Code haute performance, Preuve de programme, Optimisation source-à-source, Compilation, Logique de séparation
Mots-clés :
  • Code source (informatique)
  • Calcul intensif (informatique)
Résumé : 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.
 
Type de contenu : Text
Format : PDF
 
Entrepôt d'origine : STAR : dépôt national des thèses électroniques françaises
Identifiant : 2025STRAD013
Type de ressource : Thèse