Supervision : Antoine MINÉ

Analyse statique par interprétation abstraite de la portabilité des programmes

Le but de la thèse est de développer des nouvelles classes d'analyses statiques qui soient adaptées aux propriétés de portabilité, en particulier pour évaluer l'impact d'un changement de l'environnement sur la sémantique d'un programme.
Les logiciels informatiques tendent à être utilisés beaucoup plus longtemps et dans une plus grande variété d'environnements que prévu lors de leur conception. Si aucune précaution n'est prise, l'adaptation d'un logiciel à de nouvelles utilisations peut s'avérer très difficile et coûteuse. Assurer la portabilité des programmes est un enjeu majeur : il s'agit de s'assurer que leur compilation et leur exécution dans un environnement différent aura un effet réduit et maîtrisé sur leur sémantique, et que la sûreté d'exécution n'est pas compromise.
Le travail pourra explorer en particulier les pistes suivantes : la spécification formelle des propriétés de portabilité, les domaines abstraits pour l'analyse de portabilité, les analyses différentielles sur l'environnement, les analyses différentielles sur le code, la validation théorique et expérimentale.

2015-2021 Publications

• 2021
  • D. Delmas, A. Ouadjaout, A. Miné : “Static Analysis of Endian Portability by Abstract Interpretation”, 28^th Static Analysis Symposium (SAS 2021), vol. 12913, Lecture Notes in Computer Science, Chicago, Illinois, United States, pp. 102-123, (Springer International Publishing) (2021)
• 2019
  • D. Delmas, A. Miné : “Analysis of Software Patches Using Numerical Abstract Interpretation”, International Static Analysis Symposium, vol. 11822, Lecture Notes in Computer Science, Porto, Portugal, pp. 225-246, (Springer) (2019)
  • D. Delmas, A. Miné : “Analysis of Program Differences with Numerical Abstract Interpretation”, PERR 2019 - 3^rd Workshop on Program Equivalence and Relational Reasoning, Prague, Czechia (2019)
• 2015
  • A. Miné, D. Delmas : “Towards an industrial use of sound static analysis for the verification of concurrent embedded avionics software”, Embedded Software (EMSOFT), 2015 International Conference on, Amsterdam, Netherlands, pp. 65-74, (IEEE) (2015)