Actualités et événements

Dec 8 10:30 ₂₀₂₃

The Cubicle Fuzzy Loop: A Testing Framework for Cubicle

Vendredi 8 décembre 2023 10h30

Université Paris-Saclay, bâtiment 650, salle 435 (salle des thèses)

Résumé. L’objectif de cette thèse est d’intégrer une technique de test dans le model checker Cubicle. Pour cela, nous avons étendu Cubicle avec une boucle de Fuzzing (appelée Cubicle Fuzzy Loop – CFL). Cette nouvelle fonctionnalité remplit deux fonctions principales. Tout d’abord, elle sert d’oracle pour l’algorithme de génération d’invariants de Cubicle. Ce dernier, basé sur une exploration en avant de l’ensemble des états atteignables, était fortement limité par ses heuristiques lorsqu’elles sont appliquées à des modèles fortement concurrents. 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. Read more...

Dec 15 14:00 ₂₀₂₃

Stratégies pour la réduction forte

Vendredi 15 décembre 2023 14h

Université Paris-Saclay, bâtiment 660 (amphithéâtre) et visioconférence

Résumé: La sémantique d’un langage de programmation, et d’un langage fonctionnel en particulier, laisse généralement une certaine liberté quant à l’ordre dans lequel sont effectuées les différentes opérations. Les différentes stratégies qui peuvent être adoptées, comme l'appel par valeur ou l'évaluation paresseuse, bénéficient déjà à la fois d'un large corpus théorique et de nombreuses implémentations efficaces. Ce corpus cependant est majoritairement tourné vers un objectif d'évaluation des programmes, c'est-à-dire de production d'une valeur. Le cadre associé est celui de l'évaluation faible, dans lequel aucune évaluation n'est effectuée à l'intérieur d'une fonction qui ne serait pas totalement appliquée. En effet, dans un langage fonctionnel la fermeture représentant une telle fonction est déjà en elle-même considérée comme une valeur. Read more...

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. Read more...

Dec 21 14:00 ₂₀₂₃

Stratégies à mémoire finie dans les jeux concurrents à deux joueurs.

Jeudi 21 décembre 2023 à 14h00

Salle 1Z71, ENS Paris-Saclay, 4 avenue des sciences, 91190 Gif-sur-Yvette

Visioconférence : To be announced

Résumé. On étudie des jeux concurrents à deux joueurs de durée infinie qui se jouent de la façon suivante : chaque tour, les deux joueurs choisissent chacun une action sans connaître le choix actuel de l'adversaire. Sur un nombre de tours infini, cette procédure génère une suite infinie de paires d'actions. Cette suite est alors gagnante pour le Joueur 1 si elle appartient à l'ensemble gagnant du jeu. Read more...

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...

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...

Les journées du LMF 2023 ont eu lieu les 12 – 13 juin 2023 au Étiolles Country Club.

Read more...

Congratulations to Jacques-Henri Jourdan and his co-authors who will receive the 2023 Alonzo Church Award for their outstanding contributions to Logic and computation with the design and implementation of Iris, a higher-order concurrent separation logic framework. The Award will be presented at the 50th EATCS International Colloquium on Automata, Languages and Programming, ICALP 2023, in July.

Iris has been widely used in academia, and also in industry, e.g., by engineers at Meta to verify the core components of an interprocess communication system for a new operating system.

Read more...