Compilation interactive par des transformations source-à-source dignes de confiance

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.