Séminaires antérieurs

Programming with (Discrete and Continuous) Ordinary Differential Equations

Speaker: Olivier Bournez, LIX, École Polytechnique

Tuesday, 15 November 2022, 14:00, Room 1Z14

The Analog ThingA

Abstract: Initially motivated by understanding the computational power of various continuous-time analog models of computations, several characterizations of  complexity and computability classes have been obtained recently using ordinary differential equations. Basically, each class is characterized as the class of functions containing some basic functions, and closed by composition and various natural schemas or constructions, based on ordinary differential equations.  

This means for one direction of these proofs that we can program with ordinary differential equations.

We will provide a review of some of these recent results, and some applications. We will mainly focus on their discrete counterpart, also known as discrete ordinary differential equations, or finite differences. 

Formal Security Proofs in a Post-Quantum World

Speaker: Charlie Jacomme, Inria, Paris

Tuesday, 22 November 2022, 14:00, Room 1Z76


Abstract: In the recent years, formals methods for security and their associated tools have been used successfully both to find novel and complex attacks on many protocols [A] and to help in their standardization process. They however face a new challenge with the increasing probability of quantum computers coming into the real-world: we need to be able to provide guarantees against quantum attackers.

In this talk, we will first present a broad overview of formal methods, outlining what is the general goal of the field. We will then focus on the post-quantum issue by presenting the corresponding concrete challenges, and thus multiple ways current computational proofs of security (proof for any Polynomial Time Turing Machine attacker) can fail against a quantum attacker. We will then present the first-order logic over which Squirrel is built, the BC logic, and show based on the first part where it fails at post-quantum soundness. In a third part, we will finally present our contribution: how we made the logic and thus the Squirrel prover post-quantum sound.

Machine Learning and Autoformalisation

Speaker: Anthony Bordg, University of Cambridge

Thursday, 16 November 2022, 14:00, room 3U42


In this talk, I will describe our early achievements and future plans for increasing, through machine learning, Isabelle's competitiveness.

Verification and Synthesis of Complete Test Generation Algorithms for Finite State Machines

Speaker: Robert Sachtleben, University Bremen, Germany.

Tuesday 25 Oct 2022, 14:00, Room 1Z76

Abstract: Complete test suites are of special interest in the field of model-based testing, as they guarantee high fault detection capabilities. The variety and complexity of proposed strategies, their implementations, and their corresponding completeness arguments, however, impede thorough manual verification and practical employment.

We present a novel approach to the verification and synthesis of such strategies for models specified using finite state machines. First, we unify the presentation of several such strategies into a single framework implemented as a higher order function, which represents their shared high-level behaviour. Next, we model this framework in the interactive theorem prover Isabelle. Completeness proofs over frameworks are decoupled from concrete implementations of their parameters by suitable interfaces. This approach enables the reuse of proofs between similar strategies and simplifies implementations and completeness proofs of new variations on already handled strategies. Finally, we generate provably correct implementations of the considered test strategies. It is shown that these exhibit comparable performance to a manually developed C++ library for certain inputs.

Algorithm for Consistent Query Answering under Primary Key Constraints

Speaker: Anantha Padmanabha, ENS Ulm.

Tuesday 10 May 2022, 11:00, (salle 1Z76 ENS Paris-Saclay and online)

Abstract: Databases often have constraints. However, these days it is common to have databases that violate such constraints. Such a database is called an “inconsistent database”. One of the basic constraints is the “primary key constraint” which states there can be at most one tuple for every primary key. If a database violates primary key constraint, it will contain more than one tuple for the same primary key. In this setting, the notion of a repair is defined by picking exactly one tuple for each primary key (maximal consistent subset of the database). A Boolean conjunctive query q, is certain for an inconsistent database D if q evaluates to true over all repairs of D. In this context, we have a dichotomy conjecture that states that for a fixed boolean conjunctive query q, testing whether q is certain for an input database D is either polynomial time or coNP-complete.

The conjecture is open in general, but has been verified for self-join-free and path queries. However, the polynomial time algorithms known in the literature are complex and use different strategies in the two cases. We propose a simple inflationary fixpoint algorithm for consistent query answering which correctly computes certain answers when the query q falls in the polynomial time cases for self-join-free queries and path queries. This raises a natural question, whether this algorithm works for all polynomial time cases. We answer this negatively and show that there are polynomial time certain queries (with self-joins) which cannot be computed by such an algorithm.

This is a joint ongoing work with Diego Figueira, Luc Segoufin and Cristina Sirangelo.

Reaching Consensus in Hostile Environments

Speaker: Thomas Nowak, LISN, Université Paris-Saclay.
Friday 15 April 2022, 11:00, (room 1Z28 ENS Paris-Saclay)

Abstract: Reaching consensus in a distributed system is one of the most fundamental problems studied in distributed computing. It is non-trivial due to uncertainties related to unsuccessful communication and process faults. In particular, the celebrated FLP impossibility result shows why scheduling an event via an asynchronous communication medium such as email is difficult. In this talk, I will present our recent results on exact and approximate consensus in hostile environments such as dynamic networks (e.g., due to mobility of agents) and synthetic bacterial cultures.

Correct Blockchain-based Business Processes

Speaker: Mohamed Graiet, IBM.

Monday April 5th 2022, 11:00, (online)

Abstract: A business process is a chain of events, activities, and decisions intended to achieve a specific organizational goal. Business Process Management (BPM) is a systematic approach to improving these processes.

Blockchain refers to an emerging distributed database technology that relies on a tamper-proof list of timestamped transaction records. Particular attention is paid to the integration of this technology into business processes. This integration makes it possible to create intelligent business processes. In fact, several blockchains are used in several areas, such as cryptocurrency transactions, authenticity, and storage. They provide a way to run processes reliably even in a network without any mutual trust between its nodes. One of the most interesting concepts in blockchain technology is that of smart contracts. A smart contract can be used in the definition of collaborative business processes in general and inter-organizational in particular.

The integration of blockchain technology and business processes still faces complex issues. We are particularly interested in the problem of verifying the correctness of blockchain-based business processes.


Connected multi-agent path finding

Speaker: Francois Schwarzentruber, ENS Rennes and IRISA.

Tuesday March 29 2022, 11:00, (salle 1Z71 ENS Paris-Saclay and online)

Abstract: Motivated by the increasing appeal of robots in information-gathering missions, we study multi-agent path planning problems in which the agents must remain interconnected. We model an area by a topological graph specifying the movement and the connectivity constraints of the agents. In the first part of the talk, we study the theoretical complexity of the reachability and the coverage problems of a fleet of connected agents. We also introduce a new class called sight-moveable graphs which admit efficient algorithms. In the second part, we discuss conflict-based search and rapidly-exploring random tree.

Weakly unambiguous Parikh automata and their link to holonomic series

Speaker: Florent Koechlin, LORIA.

Monday March 28 2022, 11:00, (room 1Z61 ENS Paris-Saclay and online)

Abstract: I will talk about the connection between inherent ambiguity of formal languages and the properties of their generating series. It is a classical result that regular languages have rational generating series and that the generating series of unambiguous context-free languages are algebraic. In the eighties, Philippe Flajolet developed several tools based on this connection to prove efficiently and easily the inherent ambiguity of many context-free languages, some of which resisted the historical methods based on iterations.

In this talk I will present how these ideas relying on generating series can be extended to Parikh automata, and how they provide an algorithmic tool to decide the inclusion problem for weakly unambiguous Parikh automata. This is a joint work with Alin Bostan, Arnaud Carayol and Cyril Nicaud.

Rational Defeasible Belief Change

Speaker: Ivan Varzinczak, CRIL, Université d'Artois & CNRS, France.

Tuesday March 22 2022, 11:00, (salle 1Z71 ENS Paris-Saclay and online)

Abstract: In this talk, I will present a formal framework for modelling belief change within a non-monotonic reasoning system. Belief change and non-monotonic reasoning are two areas that are formally closely related, with recent attention being paid towards the analysis of belief change within a non-monotonic environment. In this talk, I consider the classical AGM belief change operators, contraction and revision, applied to a KLM-style defeasible setting. The investigation leads us to the formal characterisation of a number of classes of defeasible belief change operators. For the most interesting classes we need to consider the problem of iterated belief change, generalising the classical work of Darwiche and Pearl in the process. This work involves belief change operators aimed at ensuring logical consistency, as well as the characterisation of analogous operators aimed at obtaining coherence, an important notion within the field of logic-based ontologies.