La face cachée de la sûreté de fonctionnement du logiciel, par Danko Ilik (CNES)
Le développement des méthodes formelles ces dernières décennies nous a fourni des outils permettant d’arriver à des niveaux de certitude élevés en ce qui concerne l’absence de pannes systématiques telles que les erreurs de conception, de programmation ou lors de la compilation. Cependant, certains modes de pannes semblent en pratique difficiles à traiter avec ces outils et c’est en particulier le cas avec les pannes aléatoires. Dans cet exposé, on s’intéressera à quelques sujets parmi les moins traités formellement et on motivera leur importance par l’exemple de certains projets relevant de la mission du CNES.

Vérification de systèmes embarqués aérospatiaux, par Pierre Roux (ONERA)
Les avions de ligne modernes embarquent de nombreux systèmes informatiques. Certains d'entre eux, comme les commandes de vol numériques, sont critiques et justifient des efforts pour augmenter notre confiance en leur correction. Nous donnerons un aperçu de quelques activités réalisées en ce sens à l'ONERA (Office National d'Étude et de Recherche Aérospatial) à Toulouse : analyse de sûreté de fonctionnement de systèmes, aspects temps réel des processeurs multicoeurs et des réseaux embarqués, et preuve formelle de propriétés numériques.

Vérification déductive de programmes assistée par ordinateur, par Xavier Leroy (Collège de France)
La vérification déductive consiste à annoter un programme par des assertions logiques et de vérifier que ces assertions sont vraies de toute exécution du programme, avec l'aide de démonstrateurs automatiques ou interactifs.  En d'autres termes, on considère le programme comme une définition mathématique et on prouve des théorèmes à son sujet en s'aidant de la puissance de la machine.  Après un exemple de vérification utilisant l'outil Frama-C WP, nous verrons comment les assistants à la démonstration tels que Coq et Lean permettent non seulement de vérifier des programmes, mais aussi de construire les principes de raisonnement -- les «logiques de programmes» -- adaptés à divers types de propriétés que l'on veut établir.

Logique de séparation : de la gestion de la mémoire à l'établissement de protocoles personnalisés, par Armaël Guéneau (Inria Saclay, LMF)
La logique de séparation, introduite dans les années 2000 afin de simplifier la preuve de programmes impliquant des pointeurs, est une extension de la logique de Hoare dans laquelle les assertions ne représentent non plus seulement des faits logiques, mais aussi des ressources qui sont possédées pendant la preuve du programme. Nous ferons un aperçu de cette logique dans le cadre de la gestion des pointeurs en preuve de programmes, puis nous expliquerons comment des extensions plus récentes dans la logique Iris reprend l'idée des ressources afin de permettre à l'utilisateur de définir et prouver des protocoles personnalisés entre différentes parties d'un programme.

High-assurance post-quantum cryptography: the ML-KEM case, par Pierre-Yves Strub (PQShield)
Concevoir, analyser et implémenter une bibliothèque de primitives cryptographiques correcte, sécurisée et efficace est une tâche délicate. Cette dernière peut être facilitée par l'utilisation de la cryptographie assistée par ordinateur, et notamment par le développement d'outils d'analyse formelle tirant parti des avancées dans le domaine de la vérification de programmes. Lors de cet exposé, je présenterai un aperçu des développements récents en cryptographie assistée par ordinateur et comment cette dernière a permis le développement d'une implémentation sure et efficace de la primitive cryptographique post-quantique ML-KEM.