Introduction à l'analyse statique : une perspective d'interprétation abstraite

L'analyse statique de programmes, ou analyse statique, vise à découvrir les propriétés sémantiques des programmes sans les exécuter. Elle joue un rôle important dans toutes les phases de développement, y compris la vérification des spécifications et des programmes, la synthèse de code optimisé, ainsi que la refactorisation et la maintenance des applications logicielles. Ce livre offre une introduction autonome à l'analyse statique, couvrant les bases des fondements théoriques et des considérations pratiques dans l'utilisation des outils d'analyse statique. En proposant une introduction rapide et complète aux non-spécialistes, le livre comble une lacune notable dans la littérature, qui jusqu'à présent se composait en grande partie d'articles scientifiques sur des sujets avancés.

Le texte couvre les fondements mathématiques de l'analyse statique, y compris la sémantique, l'abstraction sémantique et le calcul des invariants de programme ; des notions et techniques plus avancées, y compris des techniques pour améliorer l'équilibre coût-précision de l'analyse et des abstractions pour les fonctionnalités de programmation avancées et la réponse à un large éventail de questions sémantiques ; et des techniques pour implémenter et utiliser des outils d'analyse statique. Il commence par des informations de base et une introduction intuitive et informelle aux principaux principes et techniques d'analyse statique. Il formalise ensuite les fondements scientifiques des techniques d'analyse de programmes, examine les aspects pratiques de l'implémentation et présente des applications plus avancées. Le livre peut être utilisé comme manuel dans les cours de premier et deuxième cycle en analyse statique et vérification de programmes, et comme référence pour les utilisateurs, les développeurs et les experts.