Résumé
SPARK est une technologie open source de preuve de programmes par analyse de flux de données et vérification déductive pour les programmes écrits dans le langage de programmation Ada. SPARK est codéveloppé par AdaCore, Altran et Inria, et commercialisé par AdaCore dans différents domaines critiques (avionique, militaire, spatial, ferroviaire, automobile, médical).
Dans ce séminaire, Yannick Moy a présenté les choix qui ont été faits pour le langage de spécification de SPARK et l'outil de preuve associé, les difficultés d'application en pratique, et comment l'approche de preuve auto-active y répond. Il a abordé les améliorations récentes du langage de spécification et de l'outil pour traiter les données partiellement initialisées et les pointeurs sans alias.
