### Next talks

Special talks

Wednesday February 20, 2019, 1PM, Salle 3052

**Giulio Manzonetto** (LIPN) *A syntactic and semantic analysis of program equivalences*

Special talks

Thursday February 21, 2019, 2PM, Salle 3052

**Pablo Arrighi** (Aix-Marseille Université) *Quantum, automata, computability and universality*

Special talks

Thursday February 21, 2019, 11:45AM, Salle 1007

**Samuele Giraudo** (Université Paris-Est Marne-la-Vallée) *Graded graphs and operads*

Special talks

Wednesday Mars 6, 2019, 1PM, Salle 3052

**Josef Widder** (Technische Universitaet Wien (Vienne, Autriche)) *Distributed Algorithms meet Computer-Aided Verification*

The observation that distributed algorithm theory has interesting application in computer-aided verification motivated me to explore this connection in more depth. In the second part of the talk, I will present a line of research that in the recent years led to breakthroughs in parameterized model checking of fault-tolerant broadcasting algorithms. I will close the talk by discussing ongoing research lines and open challenges.

The results on link reversal is joint work with Bernadette Charron-Bost, Matthias Fuegger, Antoine Gaillard, and Jennifer Welch. Parameterized model checking of broadcasting algorithms is joint work with Igor Konnov, Marijana Lazic, and Helmut Veith.

### Previous talks

#### Year 2019

Special talks

Thursday February 7, 2019, 1PM, Salle 3052

**Sylvain Schmitz** (LSV) *The complexity of reachability in vector addition systems*

In this talk, I will explain how some of these techniques apply to reachability in vector addition systems, a landmark result in theoretical computer science, with applications in an array of fields ranging from program verification to data logics. The decidability of the problem was first shown by Mayr thanks to a decomposition algorithm. I will present succinctly the main ideas behind a tight Ackermannian complexity upper bound obtained with Jérôme Leroux for this algorithm.

#### Year 2018

Special talks

Thursday September 20, 2018, 10:30AM, Amphi Turing (bâtiment Sophie Germain)

**Leonid Libkin** (University of Edinburgh) *Certain Answers Meet Zero-One Laws*

This measure is defined as the probability that the query is true under a random interpretation of missing information in a database. Since there are infinitely many such interpretations, to pick one at random we adopt the approach used in the study of asymptotic properties and 0-1 laws for logical sentences and define the measure as the limit of a sequence. We show that in the standard model of missing data, the 0-1 law is observed: this limit always exists and can be only 0 or 1 for a very large class of queries. Thus, query answers are either almost certainly true, or almost certainly false, and this classification behaves very well computationally. When databases satisfy constraints, the measure is defined as the conditional probability of the query being true if the constraints are true. This can now be an arbitrary rational number, which is always computable. Another refinement of the notion of certainty views answers with a larger set of interpretations that make them true as better ones. We pinpoint the exact complexity of finding best answers for first-order queries.

Special talks

Thursday July 5, 2018, 2PM, Salle 3052

**Laurent Viennot** (Inria Paris et IRIF) *Introduction to the blockchain*

Special talks

Tuesday February 20, 2018, 2PM, 3052

**Daniela Petrisan** (IRIF) *Up-To Techniques for Behavioural Metrics via Fibrations*

behavioural equivalences between systems. In this talk, I introduce up-to techniques for behavioural metrics in a coalgebraic setting and provide general results that show under which conditions such up-to techniques are sound.

For a system modelled as a coalgebra for a certain functor, the behavioural distance can be seen as a coinductive predicate using a suitable lifting of the functor. I will focus on the so called Wasserstein lifting of a functor for which we provide a new characterization in a fibrational setting. This is useful for automatically proving the soundness of up-to techniques via a generic framework developed in a previous CSL-LICS'14 paper.

I will use fibrations of predicates and relations valued in a quantale, for which pseudo-metric spaces are an example. To illustrate our framework I provide an example on distances between regular languages.

Special talks

Thursday February 1, 2018, 2PM, 3052

**Vincent Danos** (ENS) *Contractivity of Markov chains (metric couplings)*

Special talks

Tuesday January 30, 2018, 2PM, 3052

**Vincent Danos** (ENS) *Bayesian inversion and approximation*

Special talks

Thursday January 25, 2018, 2PM, 3052

**Prakash Panangaden** (McGill University) *Quantitative equational logic and free Kantorovich algebras*

Special talks

Tuesday January 23, 2018, 2PM, 3052

**Prakash Panangaden** (McGill University) *Metrics for LMPs*

Special talks

Thursday January 18, 2018, 2PM, 3052

**Prakash Panangaden** (McGill University) *A dual point of view: LMPs as function transformers*

Special talks

Tuesday January 16, 2018, 2PM, 3052

**Prakash Panangaden** (McGill University) *Introduction to LMPs: bisimulation, simulation, logical characterization*