Author: lmvadm

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)

https://www.journals.elsevier.com/journal-of-computer-languages/call-for-papers/computer-languages-for-the-internet-of-things

The goal of the DeSSUF project is the design, implementation, and the evaluation of the safety, security and ease-of-use of a new programming language for the IoT.

SIOMediC: Sécurité de l’Internet des Objets Médicaux Connectés / Security of the Internet of Medical Things