Showroom des démos

Astrée : Preuve d'Absence d'Erreurs à l'Exécution

Astrée est un analyseur statique permettant la preuve d'absence d'erreurs à l'exécution dans des programmes C critiques embarqués. Cette preuve est entièrement automatique, et est effectuée au niveau du code source, vis à vis de la sémantique du langage. Astrée a analysé avec succès des applications de taille industrielle dans le domaine aéronautique et spatial. L'analyseur Astrée a été conçu et développé au sein de l'équipe Abstraction. Il est actuellement diffusé par l'entreprise Absint Angewandte Informatik.

La démo en vidéo

  • Équipe-projet : ABSTRACTION
  • Équipe-projet commune avec l'Ecole Normale Supérieure de Paris et le CNRS

Mots-clés : Qualitification Sûreté Systèmes critiques embarqués Analyse statique Vérification Aéronautique Défense Spatial Sécurité ABSTRACTION

Haut de page