Problématique scientifique
Une erreur dans un logiciel critique peut avoir des conséquences humaines ou économiques catastrophiques, en particulier pour les systèmes embarqués. Il est donc particulièrement important de s'assurer que de tels logiciels sont sûrs avant de les mettre en service. ABSTRACTION développe des techniques d'interprétation abstraite, permettant de calculer statiquement une sur-approximation des comportements des logiciels analysés. L’analyse statique par interprétation abstraite est sûre (en cas de réussite, le logiciel analysé est effectivement prouvé correct) mais incomplète (dans certains cas, la recherche de preuve peut échouer à cause des problèmes d’indécidabilité et conduire à de fausses alarmes). En spécialisant l’analyse pour des familles de programmes bien définies, il est possible d’éliminer les fausses alarmes.

Dans ce contexte, les objectifs d’ABSTRACTION consistent à :

• formaliser des modèles sémantiques des programmes et des propriétés à prouver ;
• développer des abstractions adaptées, permettant à la fois un calcul rapide et précis, c'est-à-dire permettant la preuve effective des propriétés souhaitées ;
• implémenter et valider ces techniques par l'analyse de logiciels industriels ;
• rendre possible l'industrialisation de telles techniques à moyen terme.

Les thématiques actuelles concernent plus spécifiquement l'analyse statique précise de logiciels synchrones, quasi-synchrones et asynchrones, de systèmes biologiques et de protocoles cryptographiques.

Logiciels développés
• ASTRÉE : analyseur visant à prouver l'absence d'erreurs à l'exécution dans des programmes embarqués de type contrôle/commande avionique écrits en C.

• ProVerif et CryptoVerif : outils visant à prouver la sécurité de protocoles cryptographiques.

Fait marquant
Le logiciel ASTRÉE est utilisé pour la vérification d’absence d’erreurs à l’exécution dans les logiciels embarqués de commande de vol électrique.

Logiciels

• ASTREE
• ProVerif
• CryptoVerif

• Contrats : projets européens, contrats ACI, ANR et RNTL, contrats industriels.
• Collaborations industrielles : Airbus France, Astrium Transportation, Esterel Technologies, etc.
• Collaborations académiques : Universités de Berkeley, Harward, Vérone, École Polytechnique, École Normale Supérieure de Cachan.
• Enseignement : École Normale Supérieure, École Polytechnique, Master Parisien de Recherche en Informatique.