L'analyse statique de programmes consiste à vérifier statiquement (i.e. sans les exécuter) des propriétés dynamiques (à l'exécution) des programmes. Les classes de propriétés à vérifier sont très diverses comme la sûreté (par exemple l’absence d'erreurs à l'exécution), la vivacité (par exemple la garantie de réponse à un signal donné), la sécurité (par exemple la confidentialité d'informations traitées par un programme), etc. La grande difficulté pour démontrer automatiquement ces propriétés dynamiques réside dans le fait de trouver les bons arguments inductifs nécessaires pour en faire la preuve. Diverses solutions sont possibles : le demander à l'utilisateur (méthodes déductives), utiliser un modèle finitaire (vérification exhaustive) ou calculer l'argument inductif par approximation de la sémantique du programme (via des techniques d'approximation de point fixe de l'interprétation abstraite). Le cours explore cette dernière technique. Il en rappelle rapidement les bases avant d'explorer plusieurs abstractions infinitaires qui permettent de traiter un grand nombre d'applications à systèmes d'états infinis, qu'elles soient émergentes, classiques ou industrialisées.

Dernière mise à jour : jeudi 4 novembre 2010