Author: lmvadm

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, …).

Contribution to the Analysis of the Design-Space of a Distributed Transformation Engine

SR1 – Monday January 23, 2023, 14h

The design space for defining a distributed model transformation engine is a large spectrum of possibilities and opportunities to enhance performances in terms of computation time and memory consumption. Depending on the adopted decisions, the use of a transformation engine can be completely different (e.g., an incremental solution for an often-modified model vs a formally specified engine for reasoning, not performing). Already existing solutions propose engines with different goals based on several approaches including distribution, laziness, incrementality, and correctness. However, comparing the solutions is not trivial, and does not necessarily make sense. That is why we have implemented a new engine, integrating variability, that allows an analysis of its design space. From a language that has formal specifications, we created SparkTE, a parametrizable and distributed transformation engine on top of Spark. In this thesis, we aim at analysing the impact of the choices at different levels: the used programming models for defining expressions; the different semantics used to define the computation of a transformation; and the impact of engineering choices.

Dara Ly defended his PhD on December 5, 2022. Congratulations Dara!

Florian’s work is funded by the Agence de l’Innovation de Défense (AID) and  Région Centre Val de Loire. 

Frama-C, a framework for the analysis and verification of C programs, with its WP plugin, provides a combination of different memory models that collaborate together thanks to a smart but simple partitioning of the memory. On moderately complex, industrial strength programs, this combination already makes WP mature enough to be deployed for proving industrial critical embedded software. However, several theoretical and practical issues still persist. The goal of CoMeMoV is to tackle these issues to scale on deductive verification of complex programs. CoMeMoV, lead by Frédéric Loulergue, is a joint project of Université d’Orléans (LIFO, LMV Team), CEA List and Thales Research & Technology.

A team of 3 students from the Université d’Orléans and Université de Tours will work on the formal verification of Contiki-NG modules with Frama-C in the context of DiLLXP experience (Digital Learning Lab eXpérience Pédagogique)