News
PhD Defense Gustave Cortal
Traitement automatique des langues pour l'analyse de la subjectivité dans les récits personnels
Mardi 27 janvier 2026 à 14h00
Salle 1B36 - Amphithéâtre Simondon, 4 Av. des Sciences, 91190 Gif-sur-Yvette and online
Résumé : Les récits personnels sont des histoires que les individus racontent sur leurs propres vécus, et qui donnent à voir leurs pensées, sentiments et perceptions. Cette thèse explore des manières de modéliser l'expérience subjective dans les récits personnels à travers le traitement automatique des langues. Nous ancrons d'abord l'analyse des émotions dans les sciences cognitives : nous passons en revue les principales théories des émotions et les relions aux pratiques d'annotation dominantes. De cette synthèse émergent des pistes concrètes pour améliorer les modèles de langue, qu'il s'agisse de nouveaux schémas d'annotation, de méthodologies ou de jeux d'évaluation.
Événements passés
PhD Defense: Quentin Petitjean
Automated Tools for Inductive Reasoning in Separation Logic
Friday 30 January 2026 at 14h00
ENS Paris-Saclay, Amphi 1B26 and online
Abstract: The automated program verification aims to produce formal proofs of correctness for programs with respect to their specifications, requiring minimal user interaction. This technique is based on expressive program logics to capture the properties of programs, and algorithms or heuristics to decide satisfiablity and entailment problem for these logics. Separation logic is one of such logics, specifically designed for reasoning about programs that dynamically allocate memory and mutate this memory through pointers. To specify unbounded memory regions, separation logic includes user-defined predicates, usually expressed through inductive rules. The satisfiability and entailment problems are undecidable in general, but they are decidable for specific fragments. For instance, the PCE fragment is a restriction of the symbolic heap fragment, for which the satisfiability is decidable, where the inductively defined predicates satisfy some syntactic and semantic constraints.
This thesis proposes two extensions of the PCE fragment. The first extension defines a fragment, including the PCE one and formulæ that, although non-PCE, specify data structures that could be represented by PCE formulæ. We propose a procedure attempting to compute an equivalent PCE representation of non-PCE formulæ. We implemented this procedure and tested it on a benchmark of SL formulæ. The second extension supports the specification of overlaid data structures, i.e., data structures that share an unbounded set of locations and are therefore difficult to capture using separating conjunction. The extension, called OSL, introduces an additional operator, the overlaid separating conjunction ✪, which allows for composing heaps that share locations as long as they allocate them with distinct fields. We demonstrate that the OSL fragment has a decidable satisfiability problem.
PhD Defense: Julien Simonnet
Precise and Efficient Memory Analysis of Low-level Languages
Wednesday 17 December 2025 at 14h00
ENS Paris-Saclay, Room 1Z61 and online
Abstract: Memory safety is crucial for systems like embedded software and operating systems, where errors such as buffer overflows or use-after-free can lead to serious security issues. This thesis presents a sound, automated, and practical static analysis to prove spatial memory safety in binary code or C programs. The method builds on a novel dependent type system called TypedC which extends C's types to express complex memory properties. It works without modifying source code and uses abstract interpretation to check types and ensure spatial memory safety. A second contribution is a new framework for building relational compositional abstract domains called AADT. It enables precise analysis of complex data types like arrays, structs, and unions. The approach is implemented in the Codex platform and tested on real-world low-level code, showing strong results in verifying memory safety. Read more...
PhD Defense: Benoit Ballenghien
HOL-CSP: A Comprehensive Process Theory for Semantics and Proc-Omata Reasoning
Thursday 18 December 2025 at 14h00
ENS Paris-Saclay, Room 1B26 and online
Abstract: CSP (Concurrent Sequential Processes) is a theory for concurrent computations and interaction. HOL-CSP is a conservative embedding of CSP into Higher-order logic (HOL); this gives rise to an environment that allows formal, machine-assisted proof of behaviour which is rich in data. A particular class of processes can be seen as symbolic automata whose finite instances can be treated by a model-checker. HOL-CSP is very
expressive and allows for representing finite automata and their infinite extensions as occurring for dense time, physical systems, and parameterized process architectures. Read more...
PhD Defense Marc Renard
Contributions to FHE security against CCA adversaries
Wednesday 10 December 2025 at 14h00
CEA Nano-Innov (Building 862, Amphi 33-34) and online
Abstract: Homomorphic encryption (FHE) is a cryptographic tool allowing the delegation of computations over sensitive data while preserving its confidentiality. Unfortunately, what makes the power of FHE, its malleability (the ability to perform computations over ciphertexts), is also one weak point. On their own, homomorphic schemes only provide a relatively low security guarantee (CPA security, which models passsive adversaries) in comparison to what is usually expected (CCA2 security, which models active adversaries) from more "classical" cryptosystems. Read more...
PhD Defense: Zhuofan Xu
Permutation equivariant and permutation invariant reinforcement learning for multi-agent systems
Thursday 11 December 2025 at 9h00
ENS Paris-Saclay, Room 1Z25 and online
Abstract: Deep Reinforcement Learning (DRL) has achieved remarkable success in sequential decision-making tasks, from games to robotics. Extending DRL to Multi-Agent Reinforcement Learning (MARL) introduces additional challenges: agents must coordinate in high-dimensional environments, training becomes unstable due to non-stationarity, and learned strategies often fail to generalize across team sizes or tasks.
PhD Defence: Marin Costes
Causal graph rewriting: Space-time determinism and reversibility
Tuesday 2 December 2025 at 10h30
Amphi building 660 and online
Abstract: We study non-terminating graph rewriting models, whose local rules are applied non-deterministically---and yet enjoy a strong form of determinism, namely space-time determinism. For terminating computation, it is well-known that the property of confluence may ensure a deterministic end result. In the context of distributed, non-terminating computation however, confluence alone is too weak a property. In this thesis we provide sufficient conditions so that asynchronous local rule applications produce well-determined events in the space-time unfolding of the graph, regardless of their application orders.
PhD Defense: Josué Moreau
Programming language and formally verified compiler for low-level numerical libraries
Tuesday 25 November 2025 at 14h00
ENS Paris-Saclay, Room 1Z76 and online
Abstract: Low-level numerical libraries like GMP and BLAS are widely used. They are mostly written in C, Fortran, and Assembly, and make a heavy use of arrays and pointers. These languages are well-suited for writing efficient code but they are not safe, that is, they have many undefined behaviors, which increase the chance for bugs. Read more...
CNRS Focus on the ANR-NARCO project
The CNRS blog Focus Sciences recently published an article, “The art of modelling complex computing systems”, featuring the work of the ANR project NARCO (Non-Aggregative Resource COmpositions). The project explores new logic-based methods to model and verify complex computing systems by capturing the real interactions—sharing, dependencies and coordination—between their components. At LMF, Mihaela Sighireanu leads the lab’s contribution, focusing on verification techniques grounded in extended separation logics. This approach promises more expressive yet automatable analyses of evolving systems. Learn more on the project presentation and discover its partners: LIG, VERIMAG and LORIA.
Focus Sciences sur le projet ANR-NARCO
Le blog Focus Sciences du CNRS consacre un article, « L’art de modéliser des systèmes informatiques complexes », au projet ANR NARCO (Non-Aggregative Resource COmpositions). Ce projet développe de nouvelles approches logiques pour modéliser et vérifier des systèmes informatiques complexes, en tenant compte des interactions réelles entre leurs composants : partage, dépendances et coordination. Au LMF, Mihaela Sighireanu pilote la contribution du laboratoire, centrée sur des techniques de vérification fondées sur des logiques de séparation étendues. Cette approche vise une analyse à la fois plus expressive et plus automatisable des systèmes en évolution. Pour en savoir plus, consultez la présentation du projet et les sites de ses partenaires : LIG, VERIMAG et LORIA.
Best-Paper Award at ASYNC 2025
Raghda El Shehaby (TU Wien, Institute of Computer Engineering), Matthias Függer (LMF, CNRS, ENS Paris-Saclay), Florian Huemer (TU Wien, Institute of Computer Engineering) and Andreas Steininger (TU Wien, Institute of Computer Engineering) received the Best IEEE ASYNC Paper Award in 2025. Read more...