Author: lmvadm

mech-uvl is a Dafny formalization and C# tooling project for the Universal Variability Language (UVL)
https://github.com/mech-uvl/mech-uvl
https://doi.org/10.5281/zenodo.21003070

mechapuppet is a mechanized semantics and verified compiler for a subset of Puppet, a configuration management language.
https://github.com/MechaPuppet/mechapuppet-why3
https://hal.science/hal-05622814

Tempo is A lightweight synchronous runtime inspired by Esterel, Boussinot’s FairThreads, and ReactiveML, leveraging OCaml 5 effects to experiment with modern implementations.
https://github.com/DabrowskiFr/tempo

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.