News & Events

Le Grand prix 2023 Inria-Académie des sciences a été décerné à Gilles Dowek.

Parallèlement à ses travaux scientifiques et techniques, Gilles Dowek a contribué à la construction d'une philosophie naissante de l'informatique, qui se construit dans un dialogue entre philosophes et scientifiques. Il s'est, en particulier, intéressé à la place du calcul en mathématiques, à la différence entre les langues et les langages et aux rapports entre la thèse de Church-Turing et celle de Galilée.

— Citation du prix

Le Prix Inria – Académie des sciences récompense depuis 2013 une ou un scientifique ayant contribué de manière exceptionnelle au champ des sciences informatiques et mathématiques.

Read more...

Dec 14 9:00 ₂₀₂₃

Abstract. Many verification problems for concurrent systems have been successfully addressed by various methods over the years, particularly Petri net unfoldings. However, questions of long-term behavior and stabilization have received relatively little attention. For instance, crucial features of the long-term dynamics of ecosystems, such as basins of attraction and tipping points, remain difficult to identify and quantify with good coverage. A central reason for this is the focus, in ecological modeling, on continuous models, which provide refined simulations but do not generally allow a survey of how the system evolution would be altered under additional events or in otherwise different situations. In this work, we aimed to provide a toolkit for modeling and analyzing ecosystem dynamics. We advocate for safe contextual reset Petri nets for modeling since they have the potential to give an exhaustive possibilistic overview of the different feasible evolution scenarios. The unfolding of Petri nets provides us with the right tools to determine system trajectories leading to collapse or survival and eventually characterize those actions or inactions that help to support ecosystem stabilization. This characterization of the token’s production/consumption was used to separate minimally doomed configurations from free ones, meaning executions leading inevitably to the system’s collapse even though these executions are not identified a priori as bad ones and executions that keep the system stable, excluding bad or doomed states, respectively. The unfolding of safe reset nets and the algorithmic part for finding minimally doomed configurations have been successfully implemented in a software tool called Ecofolder and tested with some intriguing examples.

Jury:

• Alain Denise, Professor, Université Paris-Saclay (President)
• Dimitri Lefebvre, Professor, Université Le Havre Normandie (Reviewer)
• Madalena Chaves, INRIA Senior Scientist, Inria d’Université Côte d’Azur (Reviewer)
• Cédric Lhoussaine, Professor, Université de Lille (Examiner)
• Jérôme Feret, Associated Professor, ENS Paris (Examiner)
• Franck Pommereau, Professor, Université d’Évry (Co-supervisor)
• Stefan Haar, INRIA Senior Scientist, Inria Saclay (Thesis director)

Dec 18 14:00 ₂₀₂₃

Abstract. Rust is a programming language introduced in 2015, which provides the programmer with safety features regarding the use of memory. The goal of this thesis is the development of a deductive verification tool for the Rust language, by leveraging the specificities of its type system, in order to simplify memory aliasing management, among other things. Such a verification approach ensures the absence of errors during the execution of the considered programs, as well as their compliance with a formal specification of the expected functional behavior. The theoretical foundation of the approach proposed in this thesis is to use a notion of prophecy that interprets the mutable borrows in the Rust language as a current value and a future value of this borrow. The Coq proof assistant was used to formalize this prophetic encoding and prove the correctness of the associated proof obligation generation. Furthermore, the approach has been implemented in a verification software for Rust that automates the generation of proof obligations and relies on external solvers to validate these obligations. In order to support Rust iterators, an extension has been developed to manipulate closures, as well as a verification technique for iterators and combinators. The implementation has been experimentally evaluated on relevant algorithm and data structure examples. It has also been validated through a significant case study: the verification of a satisfiability modulo theories (SMT) solver.

Jury:

• Sylvain Boulmé, Grenoble INP, VERIMAG (Reviewer)
• Peter Muller, ETH Zürich (Reviewer)
• Claire Dross, Adacore (Examiner)
• Ralf Jung, ETH Zürich (Examiner)
• François Pottier, INRIA, Cambium (Examiner)
• Mihaela Sighireanu, Université Paris-Saclay, LMF (Examiner)
• Jacques-Henri Jourdan, Université Paris-Saclay, LMF (Supervisor)
• Claude Marché, Université Paris-Saclay, LMF (Supervisor)

Stéphane Demri (LMF, CNRS) and Karin Quaas (Leipzig University) received the Best-Paper Award at JELIA 2023, the 18th Edition of the European Conference on Logics in Artificial Intelligence, which is a major forum for logic-based approaches to AI. Read more...

Hubert Comon-Lundh a reçu le LICS Test-of-Time Award 2023 pour l'article Intruder Deductions, Constraint Solving and Insecurity Decision in Presence of Exclusive Or (ArXiv preprint) cosigné avec Vitaly Shmatikov (SRI International). Le prix a été partagé avec l'article connexe An NP Decision Procedure for Protocol Insecurity with XOR de Yannick Chevalier, Ralf Küsters, Michaël Rusinowitch et Mathieu Turuani.

Read more...

Hubert Comon-Lundh received the LICS Test-of-Time Award 2023 for the article Intruder Deductions, Constraint Solving and Insecurity Decision in Presence of Exclusive Or (ArXiv preprint) co-authored with Vitaly Shmatikov (SRI International). The award was shared with the related paper An NP Decision Procedure for Protocol Insecurity with XOR by Yannick Chevalier, Ralf Küsters, Michaël Rusinowitch, and Mathieu Turuani.

Cryptographic protocols rely on cryptographic primitives to achieve goals such as data privacy and data authenticity in the presence of an attacker. Their use in important applications such as communications over the Internet or credit card payments calls for the automated verification of their security. These two papers made important progress on algorithmic aspects of protocol verification with additional operators, including XOR which is widely used in real-life applications.

Specifically, these papers establish the decidability of insecurity of cryptographic protocols with XOR and other equational theories. Chevalier et al. prove membership in NP when restricted to XOR, while Comon and Shmatikov prove decidability in a broader setting. In addition to definitively settling the complexity question for these cases, the lasting value of this line of work is demonstrated by mature verification tools such as ProVerif, Tamarin, Maude-NPA, and CPSA.— Jury Laudation

Read more...

Oct 27 14:00 ₂₀₂₃

Abstract. Switched systems are dynamical systems with several operating modes, each mode being described by a differential (continuous time) or difference (discrete time) equation. Read more...

Oct 18 14:00 ₂₀₂₃

Runtime Verification of OCaml Programs

Mercredi 18 octobre 2023 14h

Université Paris-Saclay, bâtiment 660, salle 40 (amphi)

Formal verification methods, in particular when it comes to deductive verification, bring strong guarantees about the correctness of software systems. However, they require a high degree of expertise and tremendous development time. Read more...

Oct 12 14:00 ₂₀₂₃

Abstract. We study two-player antagonistic games on graphs. In such a setting, two players, Player A and Player B, start at a given state of a graph and then concurrently interact to choose a probability distribution over successor states. This process is then repeated indefinitely, thus creating an infinite sequence of states: the outcome of game. That outcome is mapped by a payoff function to a value between 0 and 1 that Player A wants to maximize, while Player B wants to minimize it.

Read more...

Sep 12 14:00 ₂₀₂₃

Read more...

Jul 4 14:00 ₂₀₂₃

Résumé : La présente thèse se situe à l'intersection des méthodes formelles et des bases de données, et s'intéresse à la formalisation de la provenance des données à l'aide de l'assistant de preuve Coq. L'étude de la provenance des données, qui permet de retracer leur origine et leur historique, est essentielle pour assurer la qualité des données, éviter les interprétations erronées et favoriser la transparence dans le traitement des données. Read more...