Verimag

Détails sur le séminaire

CTL
19 juin 2009 - 10h15
Analyse statique : de la théorie à la pratique
par David Monniaux de CNRS / VERIMAG



Résumé : Il est important que les logiciels pilotant les systèmes critiques (avions, centrales nucléaires, etc.) fonctionnent correctement — alors que la plupart des systèmes informatisés de la vie courante (micro-ordinateur, distributeur de billets, téléphone portable) ont des dysfonctionnements visibles. Il ne s'agit pas là d'un simple problème d'ingéniérie : on sait depuis les travaux de Turing et de Cook que la preuve de propriétés de bon fonctionnement sur les programmes est un problème intrinsèquement difficile.
Pour résoudre ce problème , il faut des méthodes à la fois efficaces (coûts en temps et en mémoire modérés), sûres (qui trouvent tous les problèmes possibles) et précises (qui fournissent peu d'avertissements pour des problèmes inexistants). La recherche de ce compromis nécessite des recherches faisant appel à des domaines aussi divers que la logique formelle, l'analyse numérique ou l'algorithmique « classique ».
De 2002 à 2007 j'ai participé au développement de l'outil d'analyse statique Astrée. Ceci m'a suggéré quelques développements annexes, à la fois théoriques et pratiques (utilisation de techniques de preuve formelle, analyse de filtres numériques...). Plus récemment, je me suis intéressé à l'analyse modulaire de propriétés numériques et aux applications en analyse de programme de techniques de résolution sous contrainte (programmation semidéfinie, techniques SAT et SAT modulo théorie).



HDR, Jury composé de :
- Roberto Giacobazzi, professeur à l'Université de Vérone, rapporteur
- Éric Goubault, chercheur au CEA et professeur à l'École polytechnique, rapporteur
- Andreas Podelski, professeur à l'Université Albert-Ludwigs de Freiburg, rapporteur
- Gilles Dowek, professeur à l'École polytechnique
- Roland Groz, professeur à Grenoble-INP
- Helmut Seidl, professeur à l'Université technique de Munich

Contact | Plan du site | Site réalisé avec SPIP 3.0.26 + AHUNTSIC [CC License]

info visites 874884