Evènement pour le groupe Modélisation et Verification


Date 2006-12-14  11:00-12:15
Titre L'analyseur statique Astrée 
RésuméAstrée est un analyseur statique, basé sur l'interprétation abstraite, qui vérifie l'absence d'erreurs à l'exécution pour un sous-ensemble du langage C. Astrée est sûr par construction: un sur-ensemble des comportements est calculé. Astrée est spécialisé dans l'analyse de codes synchrones réactifs de contrôle commande où il est précis et rapide (preuve d'absence de débordements de tableaux et d'erreurs arithmétiques sur les entiers et les flottants pour une application avionique critique de 400 000 lignes en 14h). Dans cet exposé, nous présenterons la méthodologie de conception d'analyseur spécialisé par raffinement des abstractions. Nous expliquerons le fonctionnement et la structure modulaire d'Astrée et donnerons quelques exemples précis de domaines abstraits qu'il nous a fallu concevoir ou adapter, tout en motivant les choix sémantiques et algorithmiques.  
LieuSalle 076, LaBRI, Rez-de-chaussée 
OrateurAntoine Miné 
EmailAntoine.Mine@ens.fr 
UrlLIENS, Paris, France 



Aucun document lié à cet événement.

Retour
Retour à l'index