Analyse statique de programmes et systèmes numériques

摘要

Alors que la complexité des traitements informatiques dans les systèmes embarqués croit chaque jour, la sûreté du fonctionnement de ces systèmes devient un enjeu crucial, tout particulièrement pour les systèmes critiques. Plus largement, synthétiser et garantir des propriétés sur le comportement d'un programme, est un objectif naturel et de large utilité. Cette habilitation (Putot, 2012) porte sur la validation automatique de propriétés numériques des programmes, par des méthodes d'analyse statique par interprétation abstraite (Cousot, Cousot, 1977).