Month: February 2023

Darine Rammal will present her work “Synchronous Cooperative Threading Model in MSSL” co-authored with Wadoud Bousdira and Frédéric Dabrowski at the The 38th ACM/SIGAPP Symposium On Applied Computing

A special issue of the International Journal of Parallel Programming edited by Virginia Niculescu and Frederic Loulergue: https://doi.org/10.1007/s10766-023-00752-x

This project is lead by Jules Chouquet.

Frama-C, une plateforme open-source d’analyses de programmes C

SR1, Monday, February 13, 2023, 13h30

Cet exposé présentera Frama-C, une plateforme open-source dédiée à l’analyse de programmes écrits en langage C. Après un aperçu général de la plateforme, nous introduirons ses principaux greffons d’analyse. Ainsi, nous expliquerons d’abord comment prouver l’absence de comportements indéfinis (ou les détecter s’il y en a) à l’aide d’Eva, le greffon d’analyse de valeurs par interprétation abstraite, nous introduirons ensuite comment prouver des propriétés fonctionnelles à l’aide du greffon WP dédié à la vérification déductive, puis nous présenterons comment détecter des erreurs avancées en cours d’exécution d’un programme, à l’aide d’E-ACSL, le greffon dédié à la vérification à l’exécution. Enfin, nous montrerons quelques usages plus avancés combinant différentes analyses. Les différentes techniques présentées seront illustrées à travers différents exemples réels provenant de domaines applicatifs variés (nucléaire, avionique, carte à puce, …).