Author: lmvadm

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.

Towards a formalization and generalization of divide-and-conquer parallel design pattern
Structuring is essential in parallel programming, as it helps manage the inherent complexity of concurrent computation. One effective way to achieve such structuring is through programming patterns and algorithmic skeletons. Among these, the divide-and-conquer pattern plays a fundamental role. It is defined by a recurrence relation that expresses the solution to a problem in terms of the solutions to smaller subproblems of the same nature. This pattern supports a wide range of computational scenarios, making it valuable to develop a general specification that captures all its possible forms and use cases. We aim to demonstrate that the divide-and-conquer pattern can be generalized in such a way that it subsumes many other parallel programming patterns. To support this claim, we propose a formal and comprehensive formulation of the divide-and-conquer paradigm. Such a generalization can serve not only theoretical purposes but also practical ones—particularly in the design of parallel programming libraries and APIs that rely on divide-and-conquer-based skeletons.

Frama-C/Eva: a concrete application of abstract interpretation
André Maroneze (CEA LIST)
July 16, 2025
The C language is widely used for critical systems, despite its memory unsafety. The Frama-C platform provides static and dynamic code analyses, based on formal verification techniques, to provide guarantees for C code bases. Between testing and full program proof, the Eva analyzer allows automatic identification of several kinds of undefined behaviors. It can be seen as an “abstract debugger”, and help understand what the code does. With some experience, it can scale up to 100k’s lines of code. This presentation will focus on practical examples, some theoretical foundations, and ongoing challenges concerning the application of abstract interpretation to C code analysis.