Séminaires

Ouverture de la journée

Introduction & Historique

Pause

Davide Catta (LIPN)

Félix Ridoux (LIP6) : Énumération des registres vulnérables aux erreurs transitoires par model-checking incrémental

Les erreurs transitoires dues aux impacts de particules constituent une vulnérabilité bien connue des circuits électroniques. Pour évaluer la robustesse de ces circuits, plusieurs méthodes basées sur la vérification formelle ont montré des résultats prometteurs, dont certaines sont déjà adoptées dans l'industrie. L’une de ces approches consiste à identifier, à l’aide d’un model-checker, l’ensemble des registres d’un circuit vulnérables aux erreurs transitoires. Dans cette présentation, nous détaillerons comment ce problème peut être traité de manière optimisée en utilisant des variantes incrémentales d'algorithmes de model-checking de l’état de l’art.

Engel Lefaucheux (Loria) : On the Monniaux Problem in abstract interpretation

The Monniaux Problem in abstract interpretation asks, roughly speaking, whether the following question is decidable: given a program P, a safety (e.g., non-reachability) specification φ, and an abstract domain of invariants D, does there exist an inductive invariant in D guaranteeing that program P meets its specification φ. The Monniaux Problem is of course parameterised by the classes of programs and invariant domains that one considers. In this talk, I’ll present a select overview and survey of work on this problem, and discuss some more recent results with respect to semilinear invariants.

Pause déjeuner salle 25-26/105

James Ortiz (LACL) : Extending Timed Automata with Clock Derivatives

The demand for large-scale, complex distributed applications is growing with the expansion of distributed computing and networking. Distributed Real-Time Applications are essential for controlling and monitoring Distributed Real-Time Systems (DRTS) in domains like aerospace, robotics, and nuclear plants. DRTS often operate on heterogeneous networks with multiple interconnected components, each equipped with independent, unsynchronized clocks. While Timed Automata (TA) and Distributed Timed Automata (DTA) are standard formalisms for modeling DRTS, they have limitations: TA assumes synchronized clocks, and DTA may fail to capture indirect interactions or dependencies between clocks fully. This paper introduces idTA, a novel, more expressive variant of TA and DTA that controls clock drift. We also present DLν, an extension of Lν logic incorporating our idTA semantics, with semantics defined over Multi-Timed Labeled Transition Systems (MLTS). We prove that model checking for DLν is EXPTIME-complete and introduce MIMETIC, a model checking tool tailored for verifying DRTS.

Vadim Malvone (LTCI) : From Theory to Practice in Natural Strategic Ability

Strategic reasoning in Multi-Agent Systems has traditionally relied on strategic logics to formalize the ability of agents to achieve temporal objectives. However, the classical representation of strategies as arbitrary functions from states to actions, while mathematically expressive, is often unrealistic for human agents or systems operating under limited cognitive or computational resources. The notion of Natural Strategic Ability introduces an alternative approach based on natural strategies, whose complexity is bounded by cognitive or computational constraints, thus making strategic reasoning and verification more faithful to real-world scenarios. In this presentation, we also report on a first attempt to implement these ideas within the VITAMIN tool, illustrating how natural strategies can be handled in practice. We conclude by outlining current limitations and discussing promising directions for future work.

Pause

Erwann Loulergue (LMF) : Passive learning of symbolic automata

Automata learning aims to find a model (in the form of an automaton) for a system's observed data, either sampled or queried. It has proved its usefulness in verification. Still, classical automata suffer from the drawback of having one transition per letter, which quickly becomes prohibitive when dealing with large alphabets (think Unicode and its 2^16 characters, or N if the letters correspond to timings). Symbolic automata allows for the handling of these large or infinite alphabets by having transitions described by predicates instead of a single letter. Learning this model has already been studied, especially in the active case, but the only previous algorithm for passive learning was mostly of theoretical interest. In this talk, I will present a novel algorithm that admits nice properties and that we think can be generalized even further than its current state.

Jaime Arias (LIPN) & Francis Hulin-Hubart (LIP6) : CosyVerif: Vers une Cohabitation des Formalismes

De plus en plus d’approches de model checking s’appuient sur des types d’entrées variés, potentiellement exprimés dans des langages ou formalismes différents. Les outils qui les implémentent ne prennent généralement en charge qu’un nombre réduit de formalismes définis à l’origine. Ils sont donc souvent ad hoc et manquent de flexibilité ainsi que de capacités d’extension et d’interopérabilité, en particulier lorsqu’il devient nécessaire d’intégrer de nouveaux formalismes. Le défi consiste alors à concevoir un moyen générique et intuitif permettant à plusieurs formalismes de coexister au sein d’un même logiciel de vérification. Ce procédé faciliterait la création, l’échange et l’interopérabilité entre formalismes, permettant ainsi d’économiser de nombreux efforts de développement. Dans cette présentation, nous introduisons CosyVerif, une plateforme en ligne capable de rassembler rapidement et simplement une grande diversité de formalismes au sein d’un cadre unifié. Elle offre également des mécanismes d’extension pour intégrer aisément de nouveaux formalismes, le tout assemblé derrière une interface graphique conviviale.