May 25-26, 2023 the team gathered at Château des Muids for a two days working session.
Author: lmvadm
[May 2023] Thierry Lecomte’s Talk
Thierry Lecomte is R&D Project Director at CLEARSY. His talks is entitled: “Formalization for securing critical applications”
When: May 17, 2023, 2PM-3PM
Where: SR1, LIFO, Université d’Orléans, France
[May 2023] CSUR Paper Accepted
Just Accepted: Component-Based Distributed Software Reconfiguration: a Verification-Oriented Survey by Hélène Coullon, Ludovic Henrio, Frédéric Loulergue, Simon Robillard
https://doi.org/10.1145/3595376
[Apr. 2023] Simon Robillard’s Talk
Analyse de boucle par quantification sur les itérations
SR3, April 18, 2023, 10:30
https://www.univ-orleans.fr/lifo/seminaire.php?lang=fr&sub=sub2#res541
[Apr. 2023] Simon Robillard’s Keynote
Automated Deduction
SR1, April 17, 2023, 13:30
https://www.univ-orleans.fr/lifo/seminaire.php?lang=fr&sub=sub2#res536
[Apr. 2023] Adrien Guatto’s Talk
Title: Une approche sous-structurelle des déformations temporelles
https://www.univ-orleans.fr/lifo/seminaire.php?lang=fr#res537
When: April 12, 2023, 10:30AM
Where: SR3, LIFO, Université d’Orléans, France
[Mar. 2023] Darine Rammal at ACM SAC 2023 in Tallinn
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
[Fev. 2023] The Special Issue on High-Level Parallel Programming and Applications 2021 appeared
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
[Feb. 2023] The SeSTeRce project is funded!
This project is lead by Jules Chouquet.
[Fev. 2023] Keynote of Julien Signoles, CEA List
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, …).