Publications

2026

• This is not a speculation, this is the reality: Reflection on Speculative Design Workshop in HCI & Design Research
  
  • Huron Samuel
  • Wei Wei
  • Tseng Wen-Jie
  • Bonnail Elise
  • Genest Eleonore
  , 2026. In this paper, we reflect on the qualities of our methods across three speculative design workshops that we designed, ran, and analyzed as part of distinct Human-Computer Interaction research projects. These workshops were conducted over the past four years and each yielded to a research publication on a different topics: visualization, virtual reality, and extended reality. Each workshop employed a different speculative framing that we define in the paper: functional, critical, and exploratory. We summarize the motivations, the process of applying speculative methods, and the outcomes of the speculation. Finally, we reflect on five qualities for speculative design research: speculative plausibility, grounding of speculation, common framing of speculation, synthesis within a framework, and the quality of reflection.
• Readability as a multi-measure construct in data visualization
  
  • Cabouat Anne-Flore
  • Huron Samuel
  • Isenberg Tobias
  • Isenberg Petra
  , 2026, pp.1-5. In this paper, we argue that readability cannot be meaningfully discussed without considering multiple complementary measures, and that relying on a single measure constitutes an epistemological choice that constrains the conclusions that can be drawn.
• PSMark: a distributed IoT benchmark for publish/subscribe under domain-based workloads
  
  • Badolato Christian
  • Samson Nathan
  • Hajj Hassan Houssam
  • Huang Chih-Kai
  • Bouloukakis Georgios
  • Pappachan Primal
  • Yus Roberto
  , 2026. The Publish/Subscribe (pub/sub) paradigm is widely used in the Internet of Things (IoT). Standalone sensors, wearables, and other devices act as producers that publish messages to consumers such as edge servers or even other IoT devices. Selecting and configuring a pub/sub protocol for an IoT system requires considering network requirements, device reliability, and required Quality-of-Service guarantees. Pub/sub benchmarking suites can help compare expected behavior of various protocols, implementations, and network configurations. However, current pub/sub benchmarks focus primarily on stress testing systems assuming mostly static configurations of homogeneous publishers which are not representative of real-world IoT deployments. To address this, we present PSMark, a distributed, multi-protocol benchmark for evaluating topic-filtered pub/sub systems under workloads representative of real-world IoT environments. PS-Mark supports (i) workloads representative of heterogeneous IoT device deployments including variations in device communication parameters, (ii) evaluation of distributed IoT deployments with multiple data aggregation servers, (iii) cross-protocol measurements across MQTT and DDS, with extensibility to additional protocols, and (iv) a modular design for adding additional metrics and interfaces. We further construct twelve IoT-focused workloads derived from seven real-world datasets in the domains of manufacturing, healthcare, smart homes, and smart cities. Finally, we benchmark five popular MQTT brokers and one DDS implementation using PSMark and analyze their performance across multiple testbeds and Quality-of-Service settings.
• Frequency-Domain Characterization of Deployed Fiber-Medium Coupling using DAS
  
  • Pruvost Pierre
  • Awwad Élie
  • Huang Heming
  • Jaouën Yves
  , 2026, pp.Th2A.59. An optical cable is monitored using a DAS interrogator and an accelerometer. Frequency-domain analysis shows that, despite notable differences beyond 100Hz, DAS still provides valuable information on the media surrounding the cable.
• Frequency-Domain Characterization of Deployed Fiber-Medium Coupling using DAS
  
  • Pruvost Pierre
  • Awwad Élie
  • Huang Heming
  • Jaouën Yves
  , 2026, pp.Th2A.59. An optical cable is monitored using a DAS interrogator and an accelerometer. Frequency-domain analysis shows that, despite notable differences beyond 100Hz, DAS still provides valuable information on the media surrounding the cable.
• Analytical Logit Scaling for High-Resolution Sea Ice Topology Retrieval from Weakly Labeled SAR Imagery
  
  • Elwaradi Reda
  • Gimenez Julien
  • Hordoir Stéphane
  • Ait Hamma Mehdi
  • Chan-Hon-Tong Adrien
  • Weissgerber Flora
  , 2026. High-resolution sea ice mapping using Synthetic Aperture Radar (SAR) is crucial for Arctic navigation and climate monitoring. However, operational ice charts provide only coarse, region-level polygons (weak labels), forcing automated segmentation models to struggle with pixel-level accuracy and often yielding under-confident, blurred concentration maps. In this paper, we propose a weakly supervised deep learning pipeline that fuses Sentinel-1 SAR and AMSR-2 radiometry data using a U-Net architecture trained with a region-based loss. To overcome the severe under-confidence caused by weak labels, we introduce an Analytical Logit Scaling method applied post-inference. By dynamically calculating the temperature and bias based on the latent space percentiles (2% and 98%) of each scene, we force a physical binarization of the predictions. This adaptive scaling acts as a topological extractor, successfully revealing fine-grained sea ice fractures (leads) at a 40-meter resolution without requiring any manual pixel-level annotations. Our approach not only resolves local topology but also perfectly preserves regional macroscopic concentrations, achieving a 78% accuracy on highly fragmented summer scenes, thereby bridging the gap between weakly supervised learning and high-resolution physical segmentation.
• Constant Time with Minimal Preprocessing, a Robust and Extensive Complexity Class
  
  • Grandjean Étienne
  • Jachiet Louis
  , 2025. In this paper, we study the class $\mathtt{cstPP}$ of operations $\mathtt{op}: \mathbb{N}^k\to\mathbb{N}$, of any fixed arity $k\ge 1$, satisfying the following property: for each fixed integer $d\ge 1$, there exists an algorithm for a RAM machine which, for any input integer $N\ge 2$, - pre-computes some tables in $O(N)$ time, - then reads $k$ operands $x_1,\ldots,x_k1$, or conversely, is reduced to $N^{\varepsilon}$, for any positive $\varepsilon<1$ (provided the set of primitive operation includes $+$, $\mathtt{div}$ and $\mathtt{mod}$). To complete the picture, we demonstrate that the $\mathtt{cstPP}$ class degenerates if the preprocessing time reduces to $N^{o(1)}$. (10.48550/ARXIV.2509.10188)
  DOI : 10.48550/ARXIV.2509.10188
• Additivity and Chain Rules for Quantum Entropies via Multi-index Schatten Norms
  
  • Fawzi Omar
  • Kochanowski Jan
  • Rouzé Cambyse
  • van Himbeeck Thomas
  Communications in Mathematical Physics, Springer Verlag, 2026, 407 (4), pp.75 (1-39). The primary entropic measures for quantum states are additive under the tensor product. In the analysis of quantum information processing tasks, the minimum entropy of a set of states, e.g., the minimum output entropy of a channel, often plays a crucial role. A fundamental question in quantum information and cryptography is whether the minimum output entropy remains additive under the tensor product of channels. Here, we establish a general additivity statement for the optimized sandwiched Rényi entropy of quantum channels. For that, we generalize the results of Devetak et al. (Commun Math Phys 266(1):37–63, 2006) to multi-index Schatten norms. As an application, we strengthen the additivity statement of Van Himbeeck and Brown (A tight and general finite-size security proof for quantum key distribution, 2025) thus allowing the analysis of time-adaptive quantum cryptographic protocols. In addition, we establish chain rules for Rényi conditional entropies that are similar to the ones used for the generalized entropy accumulation theorem of Metger et al. (Commun Math Phys 405(11):261, 2024). (10.1007/s00220-026-05567-8)
  DOI : 10.1007/s00220-026-05567-8
• Continuous AI Assistance for Model-Driven Engineering
  
  • Apvrille Ludovic
  • Sultan Bastien
  , 2026. Proactive AI-based assistants are now common in software engineering tools; however, few exist for Model-Driven Engineering (MDE) environments. Most existing AI assistants for MDE, particularly those based on large language models, require user interactions that can interrupt the modeling workflow. However, MDE is inherently a continuous process, involving successive cycles of diagram construction, verification, and modification. Relying on supplementary tools that require intensive interaction can therefore be time-consuming and disrupt engineers focus. Consequently, there is a need to shift AI-based modeling assistance paradigms to mechanisms that integrate naturally into the continuous MDE workflow. To address this need, the paper introduces ContinuousAI, a framework for AI-based continuous MDE assistance. Working alongside MDE engineers, ContinuousAI generates modeling suggestions either on demand or continuously, supporting the improvement of model quality throughout the engineering process. ContinuousAI has been implemented within the MDE toolkit TTool. Evaluation results show that ContinuousAI provides highly relevant suggestions while maintaining computation times and environmental footprints compatible with real-world continuous MDE usage.
• 5G-EcoSim: A Simulation Framework for Estimating 5G Energy Consumption Using Real-World Data and Analytical Models
  
  • Ghali Meriem
  • Busson Anthony
  • Coupechoux Marceau
  , 2026, pp.1-8. The definition and deployment of next-generation mobile networks must incorporate considerations of sustainability and environmental impact. In this context, estimating the energy consumption of a mobile network deployment across a city or region is of utmost importance. Nationwide historical aggregate values are informative but do not allow to understand the underlying dynamics or to perform prospective studies. There is hence a need for bottom-up approaches to assess the energy consumption of mobile networks. However, this is a complex task, as it depends on numerous factors, including the number and spatial distribution of base stations, the underlying technologies and their configuration, as well as user demand patterns and their geographic distribution. This paper thus introduces a simulation framework aimed at estimating the energy consumption of 5G networks at urban, regional or national scale. The framework integrates radio propagation models operating in the 3.5 GHz band with publicly available datasets describing user and base station locations, as well as network traffic volumes. As a case study, we consider the 5G deployment in France and examine the spatial distribution of network load and the resulting energy consumption. The source code and datasets are publicly available, ensuring that the simulator is fully reproducible and easily adaptable to other use cases, countries, or regions. (10.23919/WONS68803.2026.11501828)
  DOI : 10.23919/WONS68803.2026.11501828
• Capsule networks do not need to model everything
  
  • Renzulli Riccardo
  • Tartaglione Enzo
  • Grangetto Marco
  Pattern Recognition, Elsevier, 2026, 171, Part A, pp.112119 (1-11). Capsule networks are biologically inspired neural networks that group neurons into vectors called capsules, each explicitly representing an object or one of its parts. The routing mechanism connects capsules in consecutive layers, forming a hierarchical structure between parts and objects, also known as a parse tree. Capsule networks often attempt to model all elements in an image, requiring large network sizes to handle complexities such as intricate backgrounds or irrelevant objects. However, this comprehensive modeling leads to increased parameter counts and computational inefficiencies. Our goal is to enable capsule networks to focus only on the object of interest, reducing the number of parse trees. We accomplish this with REM (Routing Entropy Minimization), a technique that minimizes the entropy of the parse tree-like structure. REM drives the model parameters distribution towards low entropy configurations through a pruning mechanism, significantly reducing the generation of intra-class parse trees. This empowers capsules to learn more stable and succinct representations with fewer parameters and negligible performance loss. (10.1016/j.patcog.2025.112119)
  DOI : 10.1016/j.patcog.2025.112119
• Statistical wave field theory: Anisotropic wave fields under Neumann's boundary condition
  
  • Badeau Roland
  Journal of the Acoustical Society of America, Acoustical Society of America, 2026, 159 (3), pp.2265-2280. The statistical wave field theory mathematically establishes the statistical laws of the solutions to the wave equation in a bounded domain. It provides the closed-form expressions of the power distribution and the correlations of the wave field jointly over time, frequency, and space, which hold at high frequency and after many reflections, in terms of the geometry and the specific admittance of the boundary surface. This theory was originally developed in the particular case of mixing rooms, which are characterized by a diffuse wave field, based on the theory of dynamical billiards and on Weyl-like asymptotic laws. Then it was extended to the finite family of special polyhedra, where the wave field is anisotropic, based on a simpler geometric approach related to mathematical crystallography. In this paper, we introduce a unified version of the theory dedicated to a class of semi-mixing billiards. In the case of Neumann's boundary condition, we show that the wave field is stationary, but it is generally anisotropic. In particular, the correlation between two spatial positions at a given frequency is different from the well-known cardinal sine formula that characterizes diffuse acoustic fields. (10.1121/10.0042450)
  DOI : 10.1121/10.0042450
• Carbon Footprint of Urban 5G Traffic in Lyon Based on Real-World Data and Analytical Modeling
  
  • Ghali Mériem
  • Busson Anthony
  • Coupechoux Marceau
  Annals of Telecommunications - annales des télécommunications, Springer, 2026, pp.1-16. The deployment of 5G networks has generated significant debate regarding its environmental implications, particularly concerning carbon emissions. Although 5G technology offers improved energy efficiency per bit transmitted, concerns persist due to potential rebound effects and the significant carbon footprint associated with infrastructure deployment and baseline energy consumption. This paper presents a bottom-up approach combining a detailed radio load model and spatial distribution of users to precisely estimate the energy usage and carbon emissions of 5G networks using the 3.5 GHz band. Although the model is valid for other regions, we focus specifically on the city of Lyon in France, providing a detailed assessment of current emissions (2021-2024) and projections up to 2050, incorporating traffic growth and national energy decarbonization scenarios. At the base station scale, our results show that emissions generated by hardware manufacturing and baseline energy consumption constitute the dominant contributors to the overall carbon footprint, compared with emissions induced by traffic load. As a result, our projections indicate that an increase in traffic demand does not significantly impact the carbon footprint unless it necessitates the deployment of additional base stations. By 2050, infrastructure-related emissions could constitute up to 70% of total network emissions, highlighting a major challenge in the management of network growth to avoid rebound effect. The study demonstrates that decarbonizing electricity and enhancing energy efficiency alone are insufficient. (10.1007/s12243-026-01166-9)
  DOI : 10.1007/s12243-026-01166-9
• Multi-level Parameter Estimation for Receiver Noise in CV-QKD
  
  • Ricard Guillaume
  • Jaouën Yves
  • Alléaume Romain
  , 2026, 2743, pp.146-156. We present an experimental method for continuous-variable quantum key distribution (CV-QKD) that removes the need for conventional receiver noise calibration. By exploiting Multi-Level Parameter Estimation (MLPE) with controlled attenuation at the receiver, our approach directly estimates the total receiver noise, including contributions from the local oscillator, while simultaneously extracting channel-induced excess noise. This calibration-free technique allows continuous operation without halting quantum transmissions, increasing experimental throughput and robustness. We implement the method in a dual-polarization, local-local oscillator CV-QKD system multiplexed with a classical communication channel, demonstrating precise receiver noise estimation. Our results highlight MLPE as a practical tool for scalable, real-time CV-QKD deployment. (10.1007/978-3-032-13852-1_16)
  DOI : 10.1007/978-3-032-13852-1_16
• Decentralized Ranking Aggregation: Gossip Algorithms for Borda and Copeland Consensus
  
  • van Elst Anna
  • Le Caillec Kerrian
  • Colin Igor
  • Clémençon Stéphan
  , 2026. <div><p>The concept of ranking aggregation plays a central role in preference analysis, and numerous algorithms for calculating median rankings, often originating in social choice theory, have been documented in the literature, offering theoretical guarantees in a centralized setting, i.e., when all the ranking data to be aggregated can be brought together in a single computing unit. For many technologies (e.g. peer-to-peer networks, IoT, multi-agent systems), extending the ability to calculate consensus rankings with guarantees in a decentralized setting, i.e., when preference data is initially distributed across a communicating network, remains a major methodological challenge. Indeed, in recent years, the literature on decentralized computation has mainly focused on computing or optimizing statistics such as arithmetic means using gossip algorithms. The purpose of this article is precisely to study how to achieve reliable consensus on collective rankings using classical rules (e.g. Borda, Copeland) in a decentralized setting, thereby raising new questions, robustness to corrupted nodes, and scalability through reduced communication costs in particular. The approach proposed and analyzed here relies on random gossip communication, allowing autonomous agents to compute global ranking consensus using only local interactions, without coordination or central authority. We provide rigorous convergence guarantees, including explicit rate bounds, for the Borda and Copeland consensus methods. Beyond these rules, we also provide a decentralized implementation of consensus according to the median rank rule and local Kemenization. Extensive empirical evaluations on various network topologies and real and synthetic ranking datasets demonstrate that our algorithms converge quickly and reliably to the correct ranking aggregation. This work paves the way for principled collective decision-making in fully decentralized systems.</p></div>
• Exploiting Subgradient Sparsity in Max-Plus Neural Networks
  
  • Enaieh Ikhlas
  • Fercoq Olivier
  , 2026. Deep Neural Networks are powerful tools for solving machine learning problems, but their training often involves dense and costly parameter updates. In this work, we use a novel Max-Plus neural architecture in which classical addition and multiplication are replaced with maximum and summation operations respectively. This is a promising architecture in terms of interpretability, but its training is challenging. A particular feature is that this algebraic structure naturally induces sparsity in the subgradients, as only neurons that contribute to the maximum affect the loss. However, standard backpropagation fails to exploit this sparsity, leading to unnecessary computations. In this work, we focus on the minimization of the worst sample loss which transfers this sparsity to the optimization loss. To address this, we propose a sparse subgradient algorithm that explicitly exploits the algebraic sparsity. By tailoring the optimization procedure to the non-smooth nature of Max-Plus models, our method achieves more efficient updates while retaining theoretical guarantees. This highlights a principled path toward bridging algebraic structure and scalable learning.
• On A Class Of Dynamical Poisson-Voronoi Tessellations
  
  • Baccelli François
  • Kumar Jhawar Sanjoy
  , 2025. Consider a dynamical network model featuring mobile stations on the Euclidean plane. The initial locations of the stations are given by a homogeneous Poisson point process. The stations are all moving at a constant speed and in a random direction. Consider fixed users located in the Euclidean plane, which are served by the mobile stations. Each user stays connected to the nearest station at any given point of time. Since the stations are moving, an user disconnects and connects with different stations over time, by always selecting which ever station is the closest. This gives rise to a dynamical version of the Poisson-Voronoi tessellation. The focus of this paper is on the sequence of "handover" events of a typical user, which are the epochs when its association changes. This defines a point process on the time-axis, the "handover point process". We show that this point process is stationary and we determine its main properties, in particular its intensity and the joint distribution of its inter-event times. We also analyze the handover Palm distributions of several variables of practical interest. This includes the distance to the closest mobile stations and the point process of all other mobile stations at handover epochs. The analysis is conducted both in the single-speed and in the multi-speed scenarios. It leads to the identification of the three dimensional state variables that "Markovize" the association dynamics. The analysis is based on a specific system of non-compact particles. The motivations are in the modeling of low or medium orbit satellite wireless communication networks. The model studied here is a planar "caricature" of this problem, which is initially defined on the sphere.
• D3.2 – Certification Roadmap
  
  • Alleaume Romain
  , 2026. This document gives, in a first part, an overview of the efforts undertaken towards the security certification of Quantum Key Distribution (QKD), and presents a gap analysis of the first QKD Protection Profile published in 2023. In a second part, a new methodological framework for QKD security proof, well adapted for a furture standardization is presented, and compared to previous approaches.
• Texo: Formula Recognition within 20M Parameters
  
  • Mao Sicheng
  , 2026. In this paper we present Texo, a minimalist yet highperformance formula recognition model that contains only 20 million parameters. By attentive design, distillation and transfer of the vocabulary and the tokenizer, Texo achieves comparable performance to state-of-the-art models such as UniMERNet-T and PPFormulaNet-S, while reducing the model size by 80% and 65%, respectively. This enables real-time inference on consumer-grade hardware and even in-browser deployment. We also developed a web application to demonstrate the model capabilities and facilitate its usage for end users.
• Qiana: A First-Order Formalism to Quantify over Contexts and Formulas with Temporality
  
  • Coumes Simon
  • Paris Pierre-Henri
  • Schwarzentruber François
  • Suchanek Fabian
  Journal of Artificial Intelligence Research, Association for the Advancement of Artificial Intelligence, 2026, 85, pp.12:1-12:35. We introduce Qiana, a logic framework for reasoning on formulas that are true only in specific contexts. In Qiana, it is possible to quantify over both formulas and contexts to express, e.g., that “everyone knows everything Alice says”. Qiana also permits paraconsistent logics within contexts, so that contexts can contain contradictions. Furthermore, Qiana is based on first-order logic, and is finitely axiomatizable, so that Qiana theories are compatible with pre-existing first-order logic theorem provers. We show how Qiana can be used to represent temporality, event calculus, and modal logic. We also discuss different design alternatives of Qiana. (10.1613/jair.1.18402)
  DOI : 10.1613/jair.1.18402
• RV-Sec5: Enhancing RISC-V Security Evaluation via Targeted ISA-Level Instrumentation using gem5
  
  • Awais Muhammad
  • Mushtaq Maria
  • Naviner Lirida
  • Bruguier Florent
  • Haj Yahya Jawad
  , 2026, pp.10-19. The modularity of the RISC-V Instruction Set Architecture (ISA) has accelerated its adoption in security-critical domains, yet it introduces significant challenges for pre-silicon security validation. Current evaluation methods often rely on high-level emulation that overlooks microarchitectural side effects or post-silicon testing that identifies vulnerabilities too late in the design cycle. This paper presents RV-Sec5, a systematic framework for ISA-level security evaluation that leverages the gem5 simulator. Unlike standard simulators, RV-Sec5 introduces a methodology to map high-level security invariants-such as privilege isolation and memory protection-directly to automated, cycle-accurate instrumentation points within the ISA decoder. This approach bridges the semantic gap between abstract security policies and low-level hardware execution. We demonstrate the framework's efficacy through a case study involving unauthorized Control and Status Register (CSR) modifications, showing how RV-Sec5 detects privilege escalation attempts and monitors microarchitectural anomalies, such as TLB flushes and cache state changes, in real-time. (10.1145/3793638.3793640)
  DOI : 10.1145/3793638.3793640
• Optimal Quantum Algorithm for Gibbs State Preparation
  
  • Rouzé Cambyse
  • Stilck França Daniel
  • Alhambra Álvaro
  Physical Review Letters, American Physical Society, 2026, 136 (6), pp.060601. It is of great interest to understand the thermalization of open quantum many-body systems, and how quantum computers are able to efficiently simulate that process. A recently introduced dissipative evolution, inspired by existing models of open system thermalization, has been shown to be efficiently implementable on a quantum computer. Here, we prove that, at high enough temperatures, this evolution reaches the Gibbs state in time scaling logarithmically with system size. The result holds for Hamiltonians that satisfy the Lieb-Robinson bound, such as local Hamiltonians on a lattice, and includes long-range systems. To the best of our knowledge, these are the first results rigorously establishing the rapid mixing property of high-temperature quantum Gibbs samplers, which is known to give the fastest possible speed for thermalization in the many-body setting. We then apply our result to the problem of estimating partition functions at high temperature, showing an improved performance over previous classical and quantum algorithms. (10.1103/lhht-svmn)
  DOI : 10.1103/lhht-svmn
• DRAGON: Robust Classification for Very Large Collections of Software Repositories
  
  • Balla Stefano
  • Zacchiroli Stefano
  • Degueule Thomas
  • Falleri Jean-Rémy
  • Robbes Romain
  , 2026. The ability to automatically classify source code repositories with "topics" that reflect their content and purpose is very useful, especially when navigating or searching through large software collections. However, existing approaches often rely heavily on README files and other metadata, which are frequently missing, limiting their applicability in real-world large-scale settings. We present DRAGON, a repository classifier designed for very large and diverse software collections. It operates entirely on lightweight signals commonly stored in version control systems: file and directory names, and optionally the README when available. In repository classification at scale, DRAGON improves F1@5 from 54.8% to 60.8%, surpassing the state of the art. DRAGON remains effective even when README files are absent, with performance degrading by only 6% w.r.t. when they are present. This robustness makes it practical for real-world settings where documentation is sparse or inconsistent. Furthermore, many of the remaining classification errors are near misses, where predicted labels are semantically close to the correct topics. This property increases the practical value of the predictions in real-world software collections, where suggesting a few related topics can still guide search and discovery. As a byproduct of developing DRAGON, we also release the largest open dataset to date for repository classification, consisting of 825 thousand repositories with associated ground-truth topics, sourced from the Software Heritage archive, providing a foundation for future large-scale and language-agnostic research on software repository understanding.
• Efficient Online Variational Estimation via Monte Carlo Sampling
  
  • Chagneux Mathis
  • Müller Mathias
  • Gloaguen Pierre
  • Le Corff Sylvain
  • Olsson Jimmy
  , 2026. This article addresses online variational estimation in parametric state-space models. We propose a new procedure for efficiently computing the evidence lower bound and its gradient in a streaming-data setting, where observations arrive sequentially. The algorithm allows for the simultaneous training of the model parameters and the distribution of the latent states given the observations. It is based on i.i.d. Monte Carlo sampling, coupled with a well-chosen deep architecture, enabling both computational efficiency and flexibility. The performance of the method is illustrated on both synthetic data and real-world air-quality data. The proposed approach is theoretically motivated by the existence of an asymptotic contrast function and the ergodicity of the underlying Markov chain, and applies more generally to the computation of additive expectations under posterior distributions in state-space models.
• Towards Reliable LLM-Based Model Driven Engineering: when Full Syntax Checking and Formal Verification Join the Loop
  
  • Sultan Bastien
  • Apvrille Ludovic
  , 2026. Model-Driven Engineering facilitates the design of embedded systems by promoting abstraction and enabling early verification of design correctness. Recent approaches have integrated Large Language Models into MDE workflows to automatically generate models from textual specifications. However, these models often require extensive prompt refinement and lack formal guarantees of correctness. This paper introduces an enhanced LLM-based generation process in TTool-AI, incorporating a novel dual feedback loop that combines automated syntactic checking with formal verification of safety properties. The loop iteratively refines LLM-generated SysML block and state-machine diagrams to ensure syntactic validity and verify safety properties. First experimental evaluation on both academic and industrial-grade specifications demonstrates that the proposed mechanism reliably produces syntactically correct models, enabling direct model checking of LLM-produced models and reducing the effort required by engineers to obtain correct-by-construction designs.