To: seminaire@pauillac.inria.fr From: Francois.Pottier@inria.fr Subject: SEM - INRIA : Cristal - 30/09/04 - Paris - FR Vous pouvez maintenant vous abonner à nos annonces de séminaires http://pauillac.inria.fr/seminaires/subscribe.html S E M I N A I R E . ___ / _ _ / _ / / / \ / \ / / __| / |___ |_/ |_/ / |__ |_/ |_ ___ . / / ___ __ /_ _ / _/ /| /| _ __ __ _ _ / / / /_ / __| / / |/ | / \ /_ / / \ | / __| |___ / / __/ |_ |_/ |_ / | |_/__/ |_ |_/ |/ |_/ I N R I A - Rocquencourt Salle de conférences du bâtiment 7 Jeudi 30 septembre, 10h30 -------------- David Monniaux -------------- CNRS ====================================================================== Analyse statique de code de grande taille par interprétation abstraite ====================================================================== Certaines industries critiques développent du code de grande taille pour lequel elles aimeraient avoir des assurances, notamment l'absence d'erreurs à l'exécution. L'analyse statique par interprétation abstraite obtient des données sûres sur des programmes en en calculant une sémantique approximée. On peut par exemple ainsi démontrer automatiquement que l'ensemble des états accessibles ne contient pas d'état d'erreur. Nous nous sommes en particulier intéressés à du code avionique, contenant essentiellement des filtres et opérateurs numériques et du contrôle booléen. Les contraintes industrielles étaient: - pas de modification du code - analyse automatique sans assistance humaine. La difficulté particulière était le grand nombre de variables en virgule flottante. Nous avons développé un analyseur spécifique au domaine, ASTRÉE. Celui-ci utilise différents domaines abstraits généralistes (intervalles, octogones, partitionnements...) et des domaines spécialisés sur les filtres numériques.