INRIA a CCSD electronic archive server
Not a member yet
122212 research outputs found
Sort by
A Correct-by-Construction Checker for Validation of Railway Data
No full textInternational audienceThe objective of our work is the checking of requirements on data describing railway networks. We expose the design, the formal specification and an implementation of a program that checks such constraints, with a formal proof of correctness. That program is compiled into an executable code, linked together with some additional, non-verified code for input/output. It is experimented on significantly complex examples, showing that the efficiency of the checker is competitive with non-formally verified related tools
Euler-type approximation for the invariant measure: An abstract framework
No full textWe establish a general framework to study the rate of convergence of a Euler type approximation scheme with decreasing time steps to the invariant measure, for a general class of stochastic systems. The error is measured in general Wasserstein distances, which enables to encompass cases with non global contractivity conditions. Our main assumption is a coupling property which is expressed in terms of the one-step approximation. We show that the proposed set-up can be applied to a wide range of equations that may be law dependent, such as Langevin equations, reflected equations, Boltzmann type equations and for a recent McKean Vlasov type model for neuronal activity
Foundation models and Transformers for anomaly detection: A survey
No full textInternational audienceIn line with the development of deep learning, this survey examines the transformative role of Transformers and foundation models in advancing visual anomaly detection (VAD). We explore how these architectures, with their global receptive fields and adaptability, address challenges such as long-range dependency modeling, contextual modeling and data scarcity. The survey categorizes VAD methods into reconstruction-based, feature-based and zero/few-shot approaches, highlighting the paradigm shift brought about by foundation models. By integrating attention mechanisms and leveraging large-scale pre-training, Transformers and foundation models enable more robust, interpretable, and scalable anomaly detection solutions. This work provides a comprehensive review of state-of-the-art techniques, their strengths, limitations, and emerging trends in leveraging these architectures for VAD.</div
Mechanized Dominator Tree Certification
No full textInternational audienceIn modern compilers, many optimizations and analyses, in particular those based on the SSA form, rely on dominance information, so computing dominators efficiently is an important problem. The classic algorithm to compute dominators in a control flow graph is the one designed by Lengauer and Tarjan in 1979. Other efficient algorithms have been proposed since. Previous works formally verified less efficient algorithms, and formally validated parts of the Lengauer-Tarjan algorithm, but there is no complete formal verification or validation of any of the fast algorithms computing dominators so far. In 2016, Georgiadis and Tarjan described a method to tackle these. They defined a certificate with which it becomes easy to validate dominators. Following their method, we successfully implemented and proved correct a validator of dominators in the Rocq Prover, inside the CompCertSSA verified compiler. This is the first complete mechanized certification of a fast algorithm computing dominators
A Lazy, Concurrent Convertibility Checker
No full textInternational audienceConvertibility checking — determining whether two lambda-terms are equal up to reductions — is a crucial component of proof assistants and dependently-typed languages. Practical implementations often use heuristics to quickly conclude that two terms are or are not convertible without reducing them to normal form. However, these heuristics can backfire, triggering huge amounts of unnecessary computation. This paper presents a novel convertibility-checking algorithm that relies crucially on laziness and concurrency} Laziness is used to share computations, while concurrency is used to explore multiple convertibility subproblems in parallel or via fair interleaving. Unlike heuristics-based approaches, our algorithm always finds an easy solution to the convertibility problem, if one exists. The paper presents the algorithm in process calculus style and discusses its mechanized proof of partial correctness, its complexity, and its lightweight experimental evaluation
Data Stream Processing Effectiveness in Heterogeneous Computing Environments
No full textInternational audienceDistributed Stream Processing (DSP) systems face significant challenges when deployed in heterogeneous environments such as fog computing infrastructures. While these systems were designed for homogeneous cloud environments, their deployment across devices with varying capabilities introduces performance considerations that are not well understood. We present a systematic evaluation of Apache Flink's performance when scaling stateful operations across heterogeneous hardware. Through extensive experiments on a geodistributed testbed comprising bare-metal servers, virtual machines, and Raspberry Pi devices, we examine how different TaskManager configurations affect throughput and resource utilization. Our results reveal that Flink's default configuration mechanisms can lead to significant performance limitations in heterogeneous environments, particularly due to its resource-agnostic task assignment and hash-based partitioning strategy. We identify optimal resource configurations for different node types and quantify the performance impact of various deployment strategies. These findings highlight important considerations for DSP system design in increasingly heterogeneous computing environments
ProvSQL: A General System for Keeping Track of the Provenance and Probability of Data
No full textInternational audienceWe present the data model, design choices, and performance of ProvSQL, a general and easy-to-deploy provenance tracking and probabilistic database system implemented as a PostgreSQL extension. ProvSQL’s data and query models closely reflect that of a large core of SQL, including multiset semantics, the full relational algebra, and aggregation. A key part of its implementation relies on generic provenance circuits stored in memory-mapped files. We propose benchmarks to measure the overhead of provenance and probabilistic evaluation and demonstrate its scalability and competitiveness with respect to other state-of-the-art systems
Regional Controllability of Cellular Automata as a SAT Problem
No full textInternational audienceControllability, one of the fundamental concepts in control theory, consists in guiding a system from an initial state to a desired one within a limited (and possibly minimum) time interval. When the objective is limited to a specific sub-region of the system's domain, the concept is referred to as regional controllability.We examine this notion in the context of Boolean one-dimensional cellular automata of finite length. Depending on the local evolution rule, we investigate whether it is possible to control the evolution of the system by imposing particular values on the boundary conditions. This approach is related to key dynamical properties of CA, specifically chain transitivity and chain mixing. We show that the control problem can be formulated as a Boolean satisfiability (SAT) problem and can thus be addressed using SAT solvers. We also show how finding shortest paths in the configuration graph allows one to determine controllability properties. From our observations we can state that only peripherally-linear rules are fully controllable, while for other rules, the reachability ratio, that is, the fraction of controllable pairs of initial and final configurations, is vanishing when the system size grows.</div
Multiplicity manifolds as an opening to prescribe exponential decay : auto-regressive boundary feedback in wave equation stabilization
No full textInternational audienceExploring a more than 70 years old idea about the minimization of the spectral abscissa of linear functional differential equations, a series of recent works highlighted the insights that multiple spectral values may bring in the characterization of the decay rate for the solution of such dynamical systems. In fact, it has been shown that a spectral value of sufficiently high multiplicity tends to be dominant, in what is now known as the multiplicity-induced-dominancy (MID) property. When it is valid, this property can be remarkably helpful in the control of dynamical systems governed by functional differential equations or even some classes of partial differential equations. Beyond its simplicity, what sets it from other control methods is the valuable quantitative advantage it provides by prescribing the exact solution's decay rate. Since then, many works have been dedicated to studying the extent of the MID as well as its use in practical control applications. In this paper, apart from the extension of the MID property to difference functional equations with multiple delays, we study the case when the MID fails. In fact, despite the invalidity of the MID property, we emphasize the interest of forcing a spectral value multiplicity to derive a sharp estimate of the corresponding rightmost spectral value. To demonstrate the effectiveness of the proposed methodology, we consider the stabilization problem of the wave equation with an auto-regressive boundary feedback. By using an appropriate finite element modeling, a numerical simulation of the boundary control for the wave equation case is performed to illustrate these results through the example of vibrations' control of a long drill pipe submitted to a shock-like disturbance. The time responses show the effectiveness of the proposed approach and mainly that the decay rate can be arbitrarily selected
Phi-FEM-FNO: a new approach to train a Neural Operator as a fast PDE solver for variable geometries
No full textInternational audienceIn this paper, we propose a way to solve partial differential equations (PDEs) by combining machine learning techniques and the finite element method called phi-FEM. For that, we use the Fourier Neural Operator (FNO), a learning mapping operator. The purpose of this paper is to provide numerical evidence to show the effectiveness of this technique. We will focus here on the resolution of two equations: the Poisson-Dirichlet equation and the non-linear elasticity equations. The key idea of our method is to address the challenging scenario of varying domains, where each problem is solved on a different geometry. The considered domains are defined by level-set functions due to the use of the phi-FEM approach. We will first recall the idea of -FEM and of the Fourier Neural Operator. Then, we will explain how to combine these two methods. We will finally illustrate the efficiency of this combination with some numerical results on three test cases. In addition, in the last test case, we propose a new numerical scheme for hyperelastic materials following the phi-FEM paradigm