Bienvenue L'IRIF est une unité mixte de recherche (UMR 8243) entre le CNRS et l'Université Paris Cité, qui héberge une équipe-projet Inria. Les recherches menées à l'IRIF reposent sur l’étude et la compréhension des fondements de toute l’informatique, afin d’apporter des solutions innovantes aux défis actuels et futurs des sciences numériques. L'IRIF regroupe près de deux cents personnes. Six de ses membres ont été lauréats de l'European Research Council (ERC), trois sont membres de l'Institut Universitaire de France (IUF), deux sont membres de l'Academia Europæa, et un est membre de l'Académie des sciences. Notion du jour Réseaux Sociaux Suivez nous sur Twitter/X et LinkedIn pour suivre toute notre actualité : Actualités 27.9.2023 Grâce au travail d'Alexandra Rogova, l'équipe Automates et applications de l'IRIF, en association avec plusieurs équipes externes s'intéressant à la théorie des bases de données (au LIGM, l'ENS, Telecom Paris, etc.), relance le site et la newsletter de « Database Theory in Paris », qui centralise les évènements scientifiques de cette thématique en région parisienne. 11.9.2023 IRIF is back to school! Today, we are welcoming our 12 new permanent members to our laboratory. As part of this day, they will present their research topics to us. 14.9.2023 Après avoir eux-mêmes suivis la Fresque du Climat, des membres du laboratoire de l'IRIF formeront, en tant que facilitateurs, des élèves de L1 à la Fresque du Numérique vendredi 15 septembre. Cet atelier permet de comprendre en équipe et de manière ludique les enjeux environnementaux du numérique. 11.9.2023 Congratulations to Mohammed Foughali, who has published a paper titled “Compositional Verification of Embedded Real-Time Systems”, alongside Pierre-Emmanuel Hladik from Nantes Université/LS2N and Alexander Zuepke from the Technical University of Munich in the Journal of Systems Architecture. You can access the article here: 6.9.2023 L'IRIF est très fier d'annoncer que Geoffroy Couteau, chargé de recherche du CNRS, a obtenu un financement pour son projet ERC Starting Grant : “Overcoming Barriers and Efficiency Limitations in Secure Computation”. Pour en savoir plus sur son projet et ses ambitions : 5.9.2023 Toutes nos félicitations à Amélie Gheerbrant, maîtresse de Conférences, qui vient d'être nommée Vice-Doyenne (VD) Vies des campus et Vie étudiante au sein de l'Université Paris Cité ! edit toutes les anciennes actualités (Ces actualités sont présentées selon un classement mêlant priorité et aléatoire.) Agenda Analyse et conception de systèmes Jeudi 5 octobre 2023, 14 heures, salle séminaire, plateau Scai, 1er étage, Bâtiment Esclangon (Jussieu) Théo Zimmermann (LTCI, Télécom Paris, Institut Polytechnique de Paris) Une théorie des organisations communautaires de maintenance de paquets Dans de nombreux écosystèmes de langages de programmation, les développeurs dépendent de plus en plus de dépendances externes en open source, disponibles via des gestionnaires de paquets. Les paquets clés qui ne sont pas maintenus présentent un risque pour les projets qui en dépendent ainsi que pour les écosystèmes. Par conséquent, des initiatives communautaires peuvent émerger au sein des écosystèmes pour résoudre ce problème en adoptant les paquets clés ayant des problèmes de maintenance. Dans mon exposé, je présenterai les résultats de l'article coécrit avec Jean-Rémy Falleri et récemment publié dans Empirical Software Engineering intitulé “A Grounded Theory of Community Package Maintenance Organizations”. Le but de celui-ci était de construire une théorie de ces organisations (CPMO), notamment leur émergence et leur mode de fonctionnement. Pour ce faire, nous avons utilisé une méthodologie qualitative appelée Grounded Theory. Nous avons analysé des documents existants provenant de plusieurs CPMO, tels que des documentations et des discussions sur des forums publics, complétés par des entretiens avec des initiateurs de CPMO. Je parlerai également de mon application de ce modèle d'organisation à l'écosystème Coq, avec la création de l'organisation Coq-community, et de l'expérience acquise par ce biais. Automates Vendredi 6 octobre 2023, 14 heures, Salle 3052 Christian Choffrut Synchronous orders on the set of integers End of july 2023 Jeff Shallit asked me the following question: assuming that a synchronous automaton (two tapes read simultaneously) recognizes an ordering on the free monoid, is it decidable whether or not this ordering has infinite chains? infinite antichains? and questions of the like. I suspect(ed) that this is not the case but I started to work in the special unary case (the alphabet has a unique letter). I proved that these questions are decidable (it's easy), I characterized the orders that are linear and showed that the equivalence of two linear orders is polynomial (more interesting). I posted it on arxiv on september 19. Then I thought that I should enrich my introduction … and found out that these were (very) old results. The characterization of linear synchronous orderings on the integers is mentioned in a paper of Liu and Minnes (2009), which refers to a paper of Khoussainov and Rubin (2001) where it is implicit and is obtained as a general result on unary relations (not necessarily orderings). In my talk I will also comment on these results and propose some possible (hopefully genuinely novel!) extensions. Graph Transformation Theory and Applications Vendredi 6 octobre 2023, 15 heures, online Ryan Wisnesky (Conexus AI, San Francisco, California, USA) Functorial Data Migration In this talk we describe functorial data migration from a re-writing perspective, by way of the open-source CQL tool from categoricaldata.net. We describe how co-presheaves and their lifting problems can be finitely presented, how solving word problems in categories enables computational category theory, and some techniques for performing functorial data migration using chase algorithms. Zoom meeting registration link YouTube live stream Vérification Lundi 9 octobre 2023, 11 heures, 3052 and Zoom link Emily Clément (IRIF) Layered controller synthesis for dynamic multi-agent systems. We present a layered method to solve a multi-agent state problem, involving Timed Automata, SMT and Reinforcement Learning. The first layer of our method, based on Timed Automata, efficiently models the systems and gives us a high-level plan. Then, in a second step, we refine our model and solve it with SMT. We combining these steps and call it the SWA-SMT solver. A main issue is that it cannot be executed in real time. To overcome this, we use SWA-SMT solutions as the initial training dataset for our final step, which aims to obtain a neural network control policy. We use reinforcement learning to train the policy. We develop and show an example where the use of this initial dataset is crucial for the overall success of the method. Combinatoire énumérative et analytique Mardi 10 octobre 2023, 11 heures, Salle 381F du bâtiment Halles aux farines (ATTENTION!) Vincent Jugé (LIGM, en délégation à l'IRIF) TBA (ATTENTION exceptionnellement en salle 381F bâtiment Halles aux farines!) Algorithmes et complexité Mardi 10 octobre 2023, 11 heures, Salle 3052 Asad Raza (LIP6) MA-hardness of Geometrically Local Stoquastic Hamiltonians The Local Hamiltonian problem for stoquastic local Hamiltonians (those that avoid the sign problem) is shown to be StoqMA-complete when the interactions are algebraically local. Moreover, the problem becomes MA-complete if the Hamiltonian is also frustration-free. In this work, we extend these results, proving the hardness of the problem for Hamiltonians that are geometrically local on 1D and 2D lattices, with only nearest neighbour interactions between qudits. Preuves, programmes et systèmes Jeudi 12 octobre 2023, 10 heures 30, Salle 3052 Juliusz Chroboczek (Université Paris Cité) Non encore annoncé. Séminaire des membres non-permanents Jeudi 12 octobre 2023, 16 heures, Salle 3052 Lucie Guillou How to verify Parameterised Broadcast Networks? In a broadcast network, a node sends a message to all of its neighbors in a synchronous fashion. The communication topology is represented as a graph and each node executes a finite-state automaton. A problem of interest in verification is to determine if such a network allows for a node to reach an error state of the automaton, this is what we will call the coverability problem. When the communication topology is given, this problem is decidable, however, when it is not the case, one needs to check that for all possible communication topologies, an error state is never reached, and the problem becomes undecidable. It is the parameterised version of the coverability problem for broadcast networks, note that neither the number of nodes nor the graph is fixed. I will present this model as well as the undecidability proof before talking about a new restriction on the network aiming to regain decidability. As far as I know (this is some ongoing work), this restriction allows in some very particular cases to regain restrictions but fails in most cases. This talk will not assume any prior knowledge in verification nor in distributed networks. La syntaxe rencontre la sémantique Jeudi 12 octobre 2023, 14 heures, salle 3052 Mariana Milicich (Université Paris Cité, CNRS, IRIF) Useful Evaluation, Inductively and Quantitatively Automates Vendredi 13 octobre 2023, 14 heures, Salle 3052 Antonio Casares (LaBRI) Non encore annoncé.