Ce cours est une introduction aux fondements de la sémantique et l’analyse de programmes. Il offre les bases sur lesquelles s’appuyer pour spécifier et développer des applications sûres, construire et se servir d’outils d’analyse et de vérification. Il vise à donner une base théorique et formelle solide sur les aspects nécessaires à la vérification des applications en utilisant les techniques et les outils d'analyse statique de code. L'analyse statique permet de prédire des comportements de l’application à l’exécution. Le cours présentera des analyses de typage, des analyses par interprétation abstraite. Ces analyses s'appuient sur une sémantique formelle du langage d'écriture des programmes