Lien iCal public : https://calendar.google.com/calendar/ical/proval%40lri.fr/public/basic.ics
Seminars
Agenda
Séminaires antérieurs
Formal Verification of Finite Systems: Contributions and Adoption to security properties
Speaker: Kais Klai, LIPN, Université Sorbonne Paris Nord.
Monday 11 April 2022, 11:00, (room 1Z25 ENS Paris-Saclay and online)
Abstract: In this talk, I will present different variants of an hybrid graph structure called Symbolic Observation Graph (SOG) that preserves stutter-invariant temporal properties of finite systems. The SOG is an explicit graph where nodes are encoded symbolically with decision diagram techniques and allows on-the-fly LTL model checking. Despite its theoretical exponential complexity, it reduces in practice the state space explosion problem and performs better than explicite and symbolic exhaustive verification approaches. The second part of the talk illustrates the adoption of such a graph for the verification and the supervision of the opacity property. Finally, I will introduce a current work on model checking of vulnerability and specific properties of Blockchain smart contracts -based processes.
Electronic voting: design, attacks and proofs
Speaker: Véronique Cortier, Loria
Tuesday 14 December 2021, 11:00, (1Z56, bât ENS)
Abstract: Electronic voting aims to achieve the same properties as traditional paper based voting. Even when voters vote from their home, they should be given the same guarantees, without having to trust the election authorities, the voting infrastructure, and/or the Internet network. The two main security goals are vote privacy: no one should know how I voted; and verifiability: a voter should be able to check that the votes have been properly counted.
In this talk, we will present the Belenios voting platform, its security properties and its limitations. On a more theoretical side, we will see how recent techniques allow to compute exactly the result of an election (e.g. the winners) without leaking information about the set of ballots. Such techniques are based on Multi-Party Computations (MPC).
Structures from Quantum Relations
Speaker: Titouan Carette
Friday, 16 December 2022, 11:00, 1Z77
Abstract: The category of relations and the category of complex linear maps have a lot in common. In particular, they are both compact closed. More concretely, in the same way that any classical process can be characterized by its set of admissible behaviours, any quantum process can be characterized by one vector, a quantum state over all observable behaviours. Thus, complex vectors can be thought of as the quantum generalization of the concept of relations. In this talk, I will illustrate this quantum relation paradigm with two examples. First, I will present a model of quantum wang tiles able to represent quantum configurations obeying local constraints. Then I will outline applications to the semantics of quantum processes via a model of generalized proof nets. Finally, I will provide arguments for the extension of those approaches beyond the quantum realm.
Sleeping is Superefficient: MIS in Exponentially Better Awake Complexity
Speaker: Fabien Dufoulon
Friday, 16 December 2022, 14:00, 1Z77
Abstract:
Maximal Independent Set (MIS) is one of the fundamental and most well-studied problems in distributed graph algorithms. Even after four decades of intensive research, the best-known (randomized) MIS algorithms have O(log n) round complexity on general graphs [Luby, STOC 1986] (where n is the number of nodes), while the best-known lower bound is Ω(√(log(n)/log(log n))) [Kuhn, Moscibroda, and Wattenhofer, JACM 2016]. Breaking past the O(log n) bound or showing stronger lower bounds have been longstanding open problems.
Characterising one-player positionality for infinite duration games on graphs
Speaker: Pierre Ohlmann, IRIF
Tuesday 30 November 2021, 11:00, (Salle 1Z56, bât ENS)
Abstract: I will present a new result, asserting that a winning condition (or, more generally, a valuation) which admits a neutral letter is positional over arbitrary arenas if and only if for all cardinals there exists a universal graph which is monotone and well-founded. Here, "positional" refers only to the protagonist; this concept is sometimes also called "half-positionality".
This is the first known characterization in this setting. I will explain the result, quickly survey existing related work, show how it is proved and try to argue why it is interesting.
Routed quantum circuits
Speaker: Augustin Vanrietvelde, Imperial College London
Tuesday 23 November 2021, 11:00, (Salle 1Z31, ENS Paris-Saclay)
Abstract: I will present the results of a recently published paper. In this paper, we argue that the quantum-theoretical structures studied in several recent lines of research cannot be adequately described within the standard framework of quantum circuits. This is in particular the case whenever the combination of subsystems is described by a nontrivial blend of direct sums and tensor products of Hilbert spaces. We therefore propose an extension to the framework of quantum circuits, given by routed linear maps and routed quantum circuits. I will outline the application of this formalism to the problem of the coherent control of quantum channels, and a potential application to the study of indefinite causal order.
Formalizing mathematics in Lean
Speaker: Floris van Doorn
Tuesday 9 November 2021, 11:00, (Salle des Thèses, bâtiment 650)
Abstract: Lean's mathematical library mathlib is a rapidly growing unified library of formalized mathematics. The library contains a large part of an undergraduate math curriculum, many graduate topics, and some projects based on mathlib address more advanced topic I will give an overview of the design decisions in mathlib to make it suitable for formalizing mathematics, and some of the recent milestones in the library.
Slides: here
Verified Software Components
Speaker: Murali Sitaraman, RESOLVE Research Group, School of Computing, Clemson University, USA
Monday 8 November 2021, 15:00, (online)
Abstract: This talk will summarize over three decades of programming language and software engineering research in the RESOLVE research group. The focus of the talk will be on building verified reusable software components. The talk will cover language design, software design, and verifier design to scale up automated verification of software correctness. Some of the discussion will be devoted to efforts on incorporating the ideas in computer science education and broadening participation in computing.
Reasoning over leaks of information for Access Control of Databases
Speaker: Pierre Bourhis, CRISTAL Lille
Tuesday 16 November 2021, 11:00, (Salle 1Z56, ENS Paris-Saclay)
Abstract: Controlling the Access of Data in Database management systems is a classical problem and it has been solved through different mechanisms. One of the most common implemented in most Databases management systems is the mechanism of views, i.e defining the accessible data of a user as the result of a query. This mechanism is also used in principle in other systems such as in social networks.
Unfortunately, this approach has some defaults. Even though it does not leak any secret information, the user seeing the data can infer some of these secret data by using different knowledge such as the logical definition of the query used to define the accessible data and different property of the database.
In this talk, I will present a formalism allowing to check when a set of views do not leak any information even through this kind of attacks.
Quantum simulation and causality
Speaker: Pablo Arnault, LMF
Tuesday 2 November 2021, 11:00, (amphi 1Z18, ENS Paris-Saclay)
Abstract: In the first part of my talk, I will show that quantum automata can be used to simulate the equations of the standard model of particle physics. These quantum automata are quantum circuits on a spacetime grid, satisfying two fundamental properties: they are reversible, as all equations of fundamental physics, and local, i.e., the information at one given node comes only from neighboring nodes, so that as in fundamental physics the speed of information is bounded by the speed of light. The equations that we are able to simulate go from quantum electrodynamics to quantum field theory in curved spacetime. In the second part of my talk, I will briefly talk about causal order in quantum theory and what I intend to investigate in this direction.