Author: lmvadm

The RADyD project (Résilience par Adaptation Dynamique pour le traitement de Données / Resilience through Dynamic Adaptation for Data Processing) has been accepted and is funded by the BQR program of the University of Orléans.
It is a collaboration between the LMV (Frédéric Loulergue, Jolan Philippe) and Pamda teams (Patrick Marcel).

Eloi Perdereau joins the team as a postdoctoral researcher in the project For-CoaLa. Welcome Eloi!

On March 25, Jolan Philippe represented LMV at a conference hosted by then IAE (School of Management), organised by students of the MSI (Management of Information Systems) Master program. He shared his insights as a researcher and noted that as AI reshapes cybersecurity, system safety and formal verification are no longer optional but essential. This shift reinforces the value of the team’s research into creating secure software.

Semantics and Verification of RDMA Programs
Guillaume Ambal, Imperial College
March 27, 2026, 2PM, SR1
Remote Direct Memory Access (RDMA) is a low-latency data-transfer technology used in high-performance computing and data centres. This talk will cover several recent formalisation results, ranging from the semantics of the technology to frameworks for verifying library implementations.

Welcome!

Tomaz Kosar, Associate Professor at the University of Maribor, Slovenia, visits the LMV team for two weeks.

Vérification formelle de couches de confiance dans les logiciels : application à la TPM Software Stack
Ecole doctorale : Mathématiques, Informatique, Physique Théorique et Ingénierie des Systèmes – MIPTIS
Unité de recherche : LIFO – Laboratoire d’Informatique Fondamentale d’Orléans
Soutenance prévue le jeudi 09 octobre 2025 à 14h00
Lieu : Thales Research & Technology 1 Avenue Augustin Fresnel, 91120 Palaiseau
Salle : Auditorium

Jolan joined the LMV Team on September the 1st as an assistant professor.

Introducing Separation Logic into ACSL
Frama-C/WP is a tool implementing deductive verification on C programs annotated by properties in the ACSL language. Both WP & ACSL rely on classical Hoare Program Logic, which is known to be intrinsically limited, especially for programs with complex structures using pointers. The modern approach to deal with such programs is to use Separation Logic instead, which is more powerful than Hoare Logic, but is more difficult to use in practice, and for which there is no support from main stream automated provers, typically SMT solvers like Z3, Alt-Ergo, CVC4 or CVC5. In this talk, I would present the directions we are investigating for introducing (some ingredients from) Separation Logic into ACSL and Frama-C/WP.