L’analyse statique automatique des logiciels repose traditionnellement sur des sur-approximations du comportement des programmes afin de garantir qu’aucune trace d'exécution ne contrevient à une propriété spécifiée. Cependant, ces sur-approximations peuvent entraîner des faux positifs, qui sont particulièrement inacceptables dans des environnements non critiques.
En revanche, les approches d’inférence par sous-approximation, bien qu’elles risquent de ne pas trouver toutes les erreurs, apparaissent plus pertinentes lorsque des garanties de correction strictes ne sont pas essentielles, car elles assurent que chaque violation détectée correspond effectivement à une erreur. Cette thèse présente un cadre d’analyse statique en arrière basé sur l’interprétation abstraite, visant à réaliser une sous-approximation du comportement des programmes. Cette méthode calcule des préconditions suffisantes et peut être appliquée, par exemple, pour dériver des préconditions libérales en vue de la détection d’erreurs au moment de l’exécution ou pour inférer des contrats de code visant à garantir la correction du programme. L’approche est à la fois complète et entièrement automatisée. Les contributions de ce travail sont doubles.
Premièrement, nous étendons le modèle sémantique et les domaines abstraits afin de permettre l’analyse de langages similaires au C dans des contextes réalistes. Cela inclut l’introduction d’opérateurs de sous-approximation pour les domaines abstraits (comme les intervalles, les polyèdres et les constructions ensemblistes) ainsi que des extensions du modèle sémantique pour prendre en compte les débordements d’entiers et les instructions d’entrée. Afin de permettre une une prise en compte raisonnable de la mémoire, nous étendons à la fois le langage et son modèle sémantique afin de tenir compte des accès mémoire bas-niveau (par exemple via des pointeurs) ainsi que des allocations et des libérations dynamiques de mémoire.
Cette extension est réalisée grâce au développement d’une sémantique concrète en arrière et d’une abstraction fondée sur le domaine des cellules et une abstraction du tas basée sur l'abstraction des allocations récentes. Deuxièmement, ces avancées théoriques sont intégrées dans l’outil d’analyse statique MOPSA, où une analyse en arrière par sous-approximation est mise en œuvre pour assurer à la fois des raisonnements numériques et de mémoire.
Nous décrivons brièvement les modifications nécessaires dans l’analyseur, telles que les extensions des signatures de domaines et les mises à jour des mécanismes d’évaluation des expressions, et nous présentons une évaluation expérimentale portant sur la précision et la performance. L’outil a été testé lors de la compétition de vérification logicielle (SV-COMP), où il a montré une bonne précision dans les catégories MemSafety et NoOverflows, ayant réussi à analyser 45% des tâches. Cependant, la précision est plus faible dans les catégories ReachSafety et SoftwareSystems, en raison de la complexité accrue des propriétés à vérifier et de la taille plus grande des programmes impliqués. Bien que notre analyseur soit en général moins précis que les outils de pointe, il nécessite des ressources bien inférieures : en moyenne, les outils concurrents consomment entre 38% et 220% plus de temps. En résumé, ce travail étend les techniques d’interprétation abstraite pour l’inférence de pré-conditions suffisantes, passant d’une base théorique à une méthode pratique et applicable aux langages de programmation réels.