INRIA a CCSD electronic archive server
Not a member yet
122212 research outputs found
Sort by
Structured Deformation Modeling with Implicit Deformation Modules
No full textThis paper presents a comprehensive theoretical exploration of implicit deformation modules and their application in shape analysis, especially registration problems. The implicit deformation module framework enables the generation of advanced structured deformations in a user-friendlyand efficient manner. We establish the well-posedness of deformations generated by these modules and demonstrate the existence of solutions to the resulting registration problem. To achieve this, we introduce the notion of featured landmarks, which enables the definition of point deformations carrying features under a flow of diffeomorphisms, even when the features themselves cannot be directly transformed via a group action of diffeomorphisms. These contributions bridge the gap left by the IMODAL1 software paper [42], which provides an implementation of some of the deformation modules presented here (explicit and implicit of order one) but lacks advanced theoretical guarantees. Finally, we demonstrate how complex structured deformation models can be estimated from data, supported by practical examples
On the problem of minimizing the epidemic final size for SIR model by social distancing
No full textInternational audienceWe revisit the problem of minimizing the epidemic final size in the SIR model through social distancing of bounded intensity. In the existing literature, this problem has been considered imposing a priori interval structure on the time period when interventions are enforced. We show that when considering the more general class of controls with an L1 constraint on the confinement effort that reduces the infection rate, the support of the optimal control is still a single time interval. This shows that, for this problem, there is no benefit in splitting interventions on several disjoint time periods. However, if the infection rate is known beforehand to change with time once from one value to another one, then we show that the optimal solution could consist in splitting the interventions in at most two disjoint time periods
Mapping and explaining syntax errors with LRgrep
No full textInternational audienceLR parsers and generated parsers are often criticized for their perceived inability to produce good syntax error messages. Yet, we believe, this inability is not inherent to LR parsing or to the use of a parser generator. Instead, we claim, this perception is caused mainly by the lack of languages and tools that allow the problem of producing good syntax error messages to be addressed at a suitable level of abstraction.In this paper, we demonstrate how to use the LRgrep language and its compiler to construct good syntax error explanations for an LR parser. We focus on a toy language of arithmetic expressions, with global and local variable definitions, whose parser is built by the Menhir parser generator. The LRgrep tool helps us discover all of the error situations that this parser can encounter. The LRgrep language lets us describe each situation via a succinct pattern and provide code that constructs an explanation message for this situation. Our description of all error situations and messages fits in one page of LRgrep and OCaml code
Keep Singing the Gospel
No full textInternational audienceGospel is a strongly typed, contract based specification language for OCaml. Gospel aims to be a lightweight surface syntax for Separation Logic formulae that can be used to specify arbitrary values. It is meant to be general enough that it may be used in conjunction with whatever verification environment (or environments) the programmer prefers. Although Gospel has already been presented in previous publications, we have made improvements to its semantics, type systems and tooling ecosystem that are worth reporting on. We present these through a series of examples and their translation into GospelSL, an intermediate Separation Logic that we use to define the semantics of Gospel. From GospelSL, we show how we can automatically create a Rocq file that enables verification using CFML or Iris
It's Alive! What a Live Object Environment Changes in Software Engineering Practice
No full textInternational audienc
Area Efficient Speculative Loop Pipelining for High-Level Synthesis
No full textInternational audienceHigh-Level Synthesis (HLS) allows the automatic generation of efficient circuit designs for computation-intensive kernels, but it lacks flexibility when dealing with irregular control flow. Dynamic and speculative HLS techniques are used to address this issue. These techniques outperform state-of-the-art HLS in kernel execution times but introduce a significant area overhead. In contrast, state-of-the-art HLS easily highlights and exploits resource-sharing opportunities. In this work, we show how to adapt an existing speculative HLS approach to take advantage of well-known static resource sharing mechanisms. Our results show a decrease of the area cost by 34% on average
AdapTT: Functoriality for Dependent Type Casts
No full textInternational audienceThe ability to cast values between related types is a leitmotiv of many flavors of dependent type theory, such as observational type theories, subtyping, or cast calculi for gradual typing. These casts all exhibit a common structural behavior that boils down to the pervasive functoriality of type formers. We propose and extensively study a type theory, called AdapTT, which makes systematic and precise this idea of functorial type formers, with respect to an abstract notion of adapters relating types. Leveraging descriptions for functorial inductive types in AdapTT, we derive structural laws for type casts on general inductive type formers
Investigating the Influence of Training Difficulty on the Learning Outcomes of Medical Students
No full textInternational audienceBackground: Determining an optimal training difficulty level for the best learning outcome is a crucial goal for adaptive educational systems. The literature supports the Inverted U-shape Hypothesis, suggesting that the ideal challenge level for learning is neither too easy nor too difficult. However, this optimal point depends on the type of training and response modality and may vary across domains, necessitating thorough examination before implementing adaptive learning procedures.Objectives: This study aimed to investigate the influence of training difficulty on the learning outcomes of French medical students.Methods: Using data from a national educational platform, we explored the influence of the mean question difficulty encountered during training, relative to individual student ability, on the learning outcomes of medical students across diverse medical specialties. Importantly, the mean difficulty level varied randomly between students on this platform, mirroring a quasi-experimental design and enabling a thorough exploration of these effects. We first employed the Elo rating system to estimate the difficulty of platform questions and the evolution of students’ abilities. A linear mixed-effects model was then used, with final exam performance as the main outcome and mean relative question difficulty during training (linear and quadratic terms) as the main predictor.Results and Conclusions: Results showed a significant negative quadratic effect of mean relative difficulty on final exam performance, revealing optimal difficulty levels for each medical specialty. Additionally, the analysis demonstrated that students with high abilities displayed a more pronounced inverted U-shaped relationship between training difficulty and final exam scores. This study advances our understanding of optimal training difficulty in the complex realm of medical education by emphasizing the need to acknowledge variability across medical specialties and student abilities
Neighbor selection strategies in the wild for CDN/V2V WebRTC live streaming: Can we learn what a good neighbor is?
No full textInternational audienceA hybrid CDN/Viewer-to-Viewer (V2V) architecture is an attractive solution for HTTP (HLS) and MPEG-DASH-based live streaming providers. It combines a traditional CDN with a V2V overlay for exchanging video fragments, reducing the CDN costs while maintaining the quality of experience. This work explores machine learning models to address the key challenge of neighbor selection. Our goal is to predict the connection quality between two arbitrary viewers using features such as locality, access providers, operating systems, past CDN, and V2V throughput. The proposed solutions are validated using an A/B testing approach on our production system and demonstrate a significant improvement in key system metrics compared to the traditional locality-based methods. We observe 17% higher V2V throughput, 26% lower delay, 37% fewer lost chunks, 39% fewer rebuffering, and 20% fewer quality switches.</div
Homogeneous Unit Sliding Mode Control for Uncertain Mechanical Systems
No full textInternational audienceThis paper introduces the concept of high-order convex approximation to address uncertainties in a class of nonlinear uncertain mechanical systems. Based on this concept, the homogeneous unit sliding mode control (HUSMC) is designed to handle multiplicative and additive perturbations (uncertainties and disturbances) of the plant. By integrating this design methodology within the framework of linear matrix inequalities (LMIs), we achieve precise adjustments to control parameters, thereby enhancing tracking accuracy and stability. Numerical simulations of an uncertain mechanical system demonstrate the effectiveness of the proposed method in mitigating uncertainties and ensuring the desired control accurac