Nous interagissons de plus en plus avec des objets pilotés par des programmes. Souvent, une erreur d'exécution d'un programme ne provoque pas de situation dangereuse. Un plantage de téléphone peut être embêtant, mais est généralement sans conséquences graves. Néanmoins, il existe des programmes gérant des tâches critiques, et les échecs de ceux-ci peuvent avoir des conséquences graves. Les pays membres de l'Agence Spatiale Européenne gardent en mémoire le vol 501 d'Ariane, le premier vol de la fusée Ariane 5. Celui-ci s'est terminé prématurément après 30 secondes, lorsque le pilote automatique a guidé la fusée hors de la trajectoire prévue, et celle-ci a été détruite par sécurité. Cet événement est la conséquence d'une erreur de programmation, et a été à la date du vol en 1995 "le bug le plus cher de l'histoire". Bien que les conséquences matérielles ont été grandes, il n'y eut pas de victimes. En 2016, un programme de financement participatif automatisé (un smart contract) s'exécutant sur la blockchain Ethereum s'est révélé vulnérable. Le rôle de ce programme était de recevoir des cryptomonnaies d'utilisateurs, dans l'objectif de financer des projets. Or, celui-ci présentait une faille de sécurité, et un utilisateur malicieux a réussi à extraire une part importante de l'argent possédée par le programme. Ce piratage a pu avoir lieu, car les développeurs du programme avaient une mauvaise compréhension du langage qu'ils utilisaient. Il y avait un écart entre le comportement attendu et le comportement réel du programme. Le vol a été chiffré en dizaines de millions de dollars. S'assurer d'avoir des programmes sûrs, et qui remplissent bien les fonctions qui leur sont attribuées est naturellement un enjeu important. Dans cette thèse, nous allons nous intéresser à la définition d'analyses statiques correctes pour langages de programmation. Une analyse statique analyse du code sans l'exécuter. Elle peut garantir certaines propriétés d'un programme, par exemple, montrer qu'il n'y a pas de division par zéro. Nous souhaitons définir des analyses correctes, c'est-à-dire avec une preuve formelle, mathématique, que les analyses calculent effectivement les propriétés attendues. Pour atteindre ces objectifs, notre approche est de partir d'une description formelle d'un langage de programmation, et d'en dériver une interprétation abstraite. L'interprétation abstraite est une méthode de calcul d'approximations des comportements des programmes, et d'en déduire des propriétés sur ces programmes. Nous avons choisi les Sémantiques Squelettiques comme cadre pour formaliser des langages de programmation, car elles sont simples, mais très expressives. Une sémantique squelettique est une description partielle d'un langage. En complétant cette description, on peut obtenir une sémantique du langage, autrement dit une description mathématique de l'exécution des programmes de ce langage. Notre objectif est d'obtenir une sémantique et une interprétation abstraite à partir de la sémantique squelettique d'un langage, et de montrer que l'interprétation abstraite est une bonne approximation de la sémantique du langage.