Welcome IRIF is a research laboratory of CNRS and Université Paris Cité, also hosting one Inria project-team. The research conducted at IRIF is based on the study and understanding of the foundations of all computer science, in order to provide innovative solutions to the current and future challenges of digital sciences. IRIF hosts about 200 people. Seven of its members have been distinguished by the European Research Council (ERC), six are members of the Institut Universitaire de France IUF), two are members of the Academia Europæa, and one is member of Académie des sciences. Notion of the day Social Networks Follow us on Twitter/X, LinkedIn and Mastodon for our latest news: News 12.4.2024 The rerun of Véronique Cortier Distinguished Talk that was held on February is now available on the IRIF YouTube channel. Her subject was: “Electronic voting: design and formal verification”. 10.4.2024 Three scientific outreach projects by IRIF researchers have been selected for the 2024 edition of France-Paris Pint of Science. The idea is to discover a scientific theme or subject in a bar. Our researchers will be talking about data protection, graphs and quantum computing. 10.4.2024 IRIF is pleased to announce its second Distinguished Lecture of the year! Our invited speaker is Omer Reingold, professor of computer science at Stanford University and the director of the Simons Collaboration on the Theory of Algorithmic Fairness (Simons Foundation). He will talk about Algorithmic Fairness. Anyone interested is welcome to join us for this talk! 29.3.2024 Congratulations to Quentin Aristote, doctoral student, who won the Helena Rasiowa prize for the best student paper at the 32nd EACSL conference: Active Learning of Deterministic Transducers with Outputs in Arbitrary Monoids 27.3.2024 Marie-Josée Iarifina has joined IRIF to replace Natalia Hacquart as Finance and Accounting Manager. Come and meet her and welcome her to office 4002. 28.3.2024 The Belgian Mathematical Society (BMS) has awarded Mirna Džamonja (CNRS, IRIF, Université de Paris) with the BMS “Godeaux lecture prize”. “The prize is awarded every year, upon proposal from a BMS board member, to a prominent belgian or international mathematician who is invited to give a talk at a conference in Belgium.” Congratulations! 27.3.2024 We welcome a new research director at IRIF, Tayssir Touili. Her areas of interest are Malware Detection, Software Verification and Formal Methods. You can meet her in room 4028A. 12.3.2024 Hugo Herbelin, research director at Inria in IRIF, is organizing the next french speaking Horizon Maths day on the topic: Mathematical Proof and Software Safety. It will take place on Wednesday, March 27, 2024, from 9 a.m. to 6 p.m. at the Henri Poincaré Institute (5 rue Pierre et Marie Curie, Paris 5th), Hermite amphitheater. Free but mandatory registration: edit all the past news (These news are displayed using a randomized-priority ranking.) Agenda Higher categories, polygraphs and homotopy Friday April 19, 2024, 2PM, Salle 3058 Jovana Obradovic A Calculus for S^3-diagrams of Manifolds with Boundary n this talk, we shall introduce a calculus for a presentation of compact, orientable, connected 3-manifolds with boundary in terms of diagrams embedded in S^3 in a form akin to the standard surgery presentation of closed, orientable, connected 3-manifolds. The motivation to introduce such a presentation of manifolds is to give a completely combinatorial description of the category 3Cob, whose arrows are 3-dimensional cobordisms, which is an ongoing project. We hope this could support further investigations of faithfulness of 3-dimensional Topological Quantum Field Theories. This is a joint work with Bojana Femić, Vladimir Grujić and Zoran Petrić. Automata Friday April 19, 2024, 2PM, Salle 3052 Florent Capelli Direct Access For Conjunctive Queries with Negation Direct Access is the operation of returning, given an index j, the j-th answer of a conjunctive query Q on a given database for some given order on the answers set of Q. While this problem is #P-hard in general (wrt combined complexity), many conjunctive queries are structured enough so that for some lexicographical ordering of their answers, one can have a direct access to the answer of Q that takes polylogarithmic time in the size of the database after polynomial time precomputation. Previous work have precisely characterized the tractable classes and given fine grained lower bounds on the time needed for precomputation depending on the structure of the query. We give a generalization of these tractability results to the case of signed conjunctive queries, that is, conjunctive queries that may contain negative atoms. Our technique is based on solving the ranked access for a class of circuits that can represent relational data. Our result then follows from the fact that the tractable (signed) conjunctive queries can be transformed into polynomial size circuit. We recover the known tractable classes from the literature in the case of positive conjunctive queries using this technique and also discover new island of tractability for signed conjunctive queries. In particular, our result generalizes to the Ranked Access Problem the known tractabilities of counting the number of answers to beta-acyclic negative queries and of deciding whether a negative query with bounded nested-width has an answer. This is join work with Oliver Irwin and appeared at ICDT 2024: - ArXiv version: https://arxiv.org/abs/2310.15800 - Published version: https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2024.13 Verification Monday April 22, 2024, 11AM, 3052 (streamed) and Zoom link Sidi Mohamed Beillahi (University of Toronto) Securing Smart Contracts Through Program Synthesis In decentralized finance (DeFi), malicious adversaries were able to steal over 2 billions dollars in crypto assets over the past two years. One very common strategy malicious adversaries use is to borrow large assets through flash loans to launch their exploits against vulnerable DeFi smart contracts deployed on the Blockchain. Flash loans are loans that are only valid within a blockchain transaction and must be repaid with fees by the end of that transaction. Unlike normal loans, flash loans allow borrowers to borrow large assets without upfront collateral deposits. In this talk, I will first present a work on automated synthesis of adversarial transactions that exploit DeFi smart contracts using flash loans. To bypass the complexity of a DeFi protocol and needs for source code analysis, we propose a new technique to approximate the DeFi protocol functional behaviors using numerical methods (polynomial linear regression and nearest-neighbor interpolation). We then construct an optimization query using the approximated functions of the DeFi protocol to find an adversarial attack that is constituted of a sequence of functions invocations with optimal parameters that provides the maximum profit. To improve the accuracy of the approximation, we propose a novel counterexample driven approximation refinement technique. I will then present a followup work studying a category of DeFi attacks known as oracle manipulation attacks and the effectiveness of the current mechanisms used to protect against those attacks. I will show that those mechanisms are inadequate to ensure DeFi smart contracts safety when confronted with significant oracle deviations. I will then present a new framework to identify parameters that allow to secure DeFi smart contracts against oracle manipulation attacks. In the framework, we first perform symbolic analysis on the given contract and construct a summary model of constraints. We then leverage an SMT solver to identify parameters values that allow to secure smart contracts against oracle deviations. The talk is based on two ICSE 2024 papers that are joint works with Zhiyang Chen, Xun Deng, Andreas Veneris, and Fan Long (University of Toronto) and Cyrus Minwalla and Han Du (Bank of Canada). Algorithms and complexity Tuesday April 23, 2024, 11AM, Salle 3052 Team Event AlgoComp lightning talks ⚡️ Distributed algorithms and graphs Tuesday April 23, 2024, 2PM, 3052 Sophie Germain Cléophée Robin (G-Scop) To be announced. One world numeration seminar Tuesday April 23, 2024, 2PM, Online Shunsuke Usuki (Kyoto University) On a lower bound of the number of integers in Littlewood's conjecture Littlewood's conjecture is a famous and long-standing open problem which states that, for every $(\alpha,\beta) \in \mathbb{R}^2$, $n\|n\alpha\|\|n\beta\|$ can be arbitrarily small for some integer $n$. This problem is closely related to the action of diagonal matrices on $\mathrm{SL}(3,\mathbb{R})/\mathrm{SL}(3,\mathbb{Z})$, and a groundbreaking result was shown by Einsiedler, Katok and Lindenstrauss from the measure rigidity for this action, saying that Littlewood's conjecture is true except on a set of Hausdorff dimension zero. In this talk, I will explain about a new quantitative result on Littlewood's conjecture which gives, for every $(\alpha,\beta) \in \mathbb{R}^2$ except on sets of small Hausdorff dimension, an estimate of the number of integers $n$ which make $n\|n\alpha\|\|n\beta\|$ small. The keys for the proof are the measure rigidity and further studies on behavior of empirical measures for the diagonal action. Non-permanent members' seminar Thursday April 25, 2024, 4PM, Salle 3052 Etienne Objois To be announced. Verification Monday April 29, 2024, 11AM, 3052 and Zoom link Niklas Kochdumper (IRIF) Neural Network Verification using Polynomial Zonotopes Since artificial intelligence is nowadays also increasingly applied in safety-critical applications such as autonomous driving and human robot collaboration, there is an urgent need for approaches that can efficiently verify that the corresponding neural networks are safe. In general, verification tasks involving neural networks can be classified into the two groups open-loop verification and closed-loop verification. For open-loop verification one aims to prove certain properties of a standalone neural network, while for closed-loop verification the neural network acts as a controller for a dynamic system. This presentation demonstrates a novel verification technique that is based on a polynomial abstraction of the input-output-relation of the single neurons, which proves to be beneficial for both open- as well as closed-loop neural network verification. Enumerative and analytic combinatorics Tuesday April 30, 2024, 11AM, Salle 3058 Viviane Pons (LISN Univ. Paris Saclay) A venir Distributed algorithms and graphs Tuesday April 30, 2024, 3:15PM, 3052 Sophie Germain Gianlorenzo D'Angelo (GSSI) Sparse Temporal Spanners with Low Stretch A temporal graph is an undirected graph G = (V,E) along with a function that assigns a time-label to each edge in E. A path in G such that the traversed time-labels are non-decreasing is called a temporal path. Accordingly, the distance from u to v is the minimum number of edges of a temporal path from u to v. A temporal alfa-spanner of G is a (temporal) subgraph H that preserves the distances between any pair of vertices in V, up to a multiplicative stretch factor of alfa. The size of H is measured as the number of its edges. In this work, we study the size-stretch trade-offs of temporal spanners. In particular we show that temporal cliques always admit a temporal (2k-1)-spanner with \tilde{O}(kn^{1+1/k}) edges, where k > 1 is an integer parameter of choice and n is the number of nodes in G. Choosing k = log n, we obtain a temporal O(log n)-spanner with \tilde{O}(n) edges that has almost the same size (up to logarithmic factors) as the temporal spanner given in [Casteigts et al., JCSS 2021] to preserve temporal connectivity. We then turn our attention to general temporal graphs. Since \Omega(n^2) edges might be needed by any connectivity-preserving temporal subgraph [Axiotis et al., ICALP'16], we focus on approximating distances from a single source. We show that \tilde{O}(n/log(1+epsilon)) edges suffice to obtain a stretch of (1+epsilon), for any small epsilon > 0. This result is essentially tight in the following sense: there are temporal graphs G for which any temporal subgraph preserving exact distances from a single-source must use \Omega(n^2) edges.