Séminaires antérieurs

Partially commuting pushdowns and rational trace relations

Speaker: Dietrich Kuske, Technische Universität Ilmenau

Tuesday, 5 September 2023, 14:00, Room 1Z34

We consider the reachability problem for pushdown systems where the pushdown does not store a word, but a Mazurkiewicz trace. Since this model generalizes multi-pushdown systems, the reachability problem can only be solved for a restricted class that we call cooperating multi-pushdown systems (cPDS). In the talk, I will show how the saturation algorithm by Finkel et al. (1997) can be modified. For such saturated cPDS, the reachability relation can be shown to be a finite union of finite compositions of prefix-recognizable trace relations (for words, these relations were studied, e.g., by Caucal, 1992).


Some challenges in quantum computing for linear algebra algorithms and data structures

Speaker: Marc Baboulin, Université Paris-Saclay

Tuesday, 12 September 2023, 14:00, Room 1Z34

Quantum computing aims at addressing computations that are currently intractable by conventional supercomputers but it is also a promising technology for speeding up some existing simulations. However it is commonly accepted that quantum algorithms will be essentially ``hybrid'' with some tasks being executed on the quantum processor while others will remain treated on classical processors (CPU, GPU,...). Among the crucial tasks achieved on classical computers, several require efficient linear algebra algorithms.


Building a Provenance-Aware Database Management System

Speaker: Pierre Senellart, ENS Ulm, head of the Valda joint CNRS, ENS, Inria project-team

Tuesday, 4 July 2023, 10:30, 1Z14

We describe ProvSQL, software currently being developed in our team that adds support for provenance management to a regular database management system, PostgreSQL. We first explain what provenance is, applications thereof, and how provenance of database queries can be defined and captured. We insist on one particular application of provenance, probabilistic query evaluation. We then explain research and engineering challenges in implementing techniques from the scientific literature on provenance management and probabilistic databases within a major database management system.

Formal Proofs for Trajectory Computation in the Plane with Straight Obstacles

Speaker: Yves Bertot, INRIA Antipolis

Tuesday, 4 July 2023, 9:20, 1Z14

Our goal is to describe smooth trajectories for robots, so that these robots don't have to stop to change direction. Several formats of trajectories could be used, but we decided to focus on trajectories given by Bézier curves. It happens that these curves have mathematical properties that make it easy to verify formally that there are no collisions. Work in collaboration with Quentin Vermande (ENS, Paris) and Reynald Affeldt (AIST, Tokyo, Japan).

Keynote: Verification of Stateful Security Protocols in Isabelle/HOL

Speaker: Achim Brucker, Chair of Computer Security, University Exeter, GB

Tuesday May 16 2023, 14:00, Room 1Z61

Communication networks like the Internet form a large distributed system where a huge number of components run in parallel, such as security protocols and distributed web applications. For what concerns security, it is obviously infeasible to verify them all at once as one monolithic entity; rather, one has to verify individual components in isolation.

While many typical components like the security protocol TLS have been studied intensively, there exists much less research on analyzing and ensuring the security of the composition of security protocols. This is a problem since the composition of systems that are secure in isolation can easily be insecure.

The verification of security protocols is one of the success stories of formal methods. There is a wide spectrum of methods available, ranging from fully automated methods to interactive theorem proving with proof assistants like Isabelle/HOL. Read more...

Minimal Generating Sets for Semiflows

Speaker: Gerard Memmi LTCI, Telecom-Paris, Institut polytechnique de Paris

Tuesday, 23 Mai 2023, 14:00, Room 1Z56 and Zoom

We discuss important characteristics of finite generating sets for F+, the set of all semiflows with non-negative coordinates of a Petri Net. We endeavor to regroup a number of algebraic results dispersed throughout the Petri Nets literature and also to better position the re- sults while considering semirings such as N or Q+ then fields such as Q. As accurately as possible, we provide a range of new algebraic results on minimal semiflows, minimal supports, and finite minimal generating sets for a given family of semiflows. Minimality of semiflows and of sup- port are critical to develop effective analysis of invariants and behavioral properties of Petri Nets. Main results are concisely presented in a table and our contribution is highlighted. We conclude with the analysis of an example drawn from the telecommunication industry underlining the efficiency brought by using minimal semiflows of minimal supports.

Co-verification for robotics: from simulation to verification

Speaker: Pedro Ribeiro Research Fellow, University of York

Tuesday, 6 June 2023, 14:00, 1Z71

Robots are expected to play important roles in furthering prosperity, however providing formal guarantees on their (safe) behaviour is not yet fully within grasp given the multifaceted nature of such cyber-physical systems. Simulation, favoured by practitioners, provides an avenue for experimenting with different scenarios before committing to expensive tests and proofs. In this talk, I will discuss how models may be brought together for (co-)verification of system properties, with simulation complementing verification. This will be cast using the model-driven RoboStar framework, that clearly identifies models of the software, hardware, and scenario, and has heterogeneous formal semantics amenable to verification using state-of-the-art model-checkers and theorem provers, such as Isabelle/UTP.

Pedro Ribeiro will be visiting the LMF the entire day - interactions welcome.

On the edit distance between transducers

Speaker: C. Aiswarya, CMI

Wednesday, 19 April 2023, 16:00, 1Z56 ENS Nord and Zoom

Abstract: Given a metric over words, define the distance between two transducers with identical domain as the supremum of the distances of their respective outputs over all inputs. This is a useful generalisation for comparing transducers that goes beyond the equivalence problem. Two transducers are said to be close (resp. k-close) if their distance is bounded (resp. at most k). We will discuss the decidability of the problem that asks whether two given transducers are close (resp. k-close), for common edit distances.

This is a joint work with Amaldev Manuel and Saina Sunny.

Aiswarya will be at LMF from 2 April to 2 June 2023 as a Visiting Professor of ENS Paris-Saclay.

String constraints with subword ordering: complexity of satisfiability

Speaker: C. Aiswarya, CMI

Monday, 17 April 2023, 15:00, Salle 1Z14 and Zoom

Abstract: We consider a variant of string constraints given by membership constraints in context-free languages and subword relation between variables. The satisfiability problem for this variant turns out to be undecidable. We consider a fragment in which the subword-order constraints do not impose any cyclic dependency between variables. We show that this fragment is \nexptime-complete. As an application of our result, we settle the complexity of control state reachability in acyclic lossy channel pushdown systems, which was shown to be decidable in Atig-Bouajjani-Touilli-08. We show that this problem is \nexptime-complete.

This is a joint work with Prakash Saivasan and Soumodev Mal, which appeared in LICS 22.

Aiswarya will be at LMF from 2 April to 2 June 2023 as a Visiting Professor of ENS Paris-Saclay.

The Future of Model-based Testing

Speaker: Jan Peleska, Universität Bremen, Saarbrücken, Germany

Friday 17 March 2023, 14:00, Room 1Z56

Abstract: Since the 1970s, model-based testing (MBT) has been comprehensively investigated in the research communities, and its industrial application has been fostered for at least two decades. Though convincing success stories about MBT have been published, we have to admit that its acceptance in industry is still not as good as it should be. This is reflected, for example, by the facts that commercial MBT tools are not selling as well as had been originally envisaged by the “campaigners of MBT” (such as myself) and that MBT has not been integrated into the verification plans of the key players in the embedded systems world. Read more...