Journées 2024 du GT Scalp Du 18 au 20 novembre 2024 à Lille Introduction Oratrices et orateurs invités Inscriptions et propositions d'exposé Informations pratiques Programme Liste des exposés contribués Participants Comité d'organisation Introduction Les rencontres 2024 du GT Scalp se tiendront à Lille du 18 au 20 novembre. Cette année, nos rencontres annuelles sont organisées conjointement avec le GT Verif du GDR-IFM qui suivront immédiatement, deux demi-journées étant organisées en commun aux deux GT, les mardi après-midi et mercredi matin: l'événement global Scalp-Verif s'étendra donc du 18 novembre au 21 novembre. Les journées SCALP débuteront lundi en milieu de journée et s'achèveront mercredi en début d'après-midi: Lundi après-midi et mardi matin seront consacrées à des journées spécifiquement SCALP; Mardi après-midi et mercredi matin seront consacrées à des journées conjointes SCALP-Vérif; Mercredi après-midi et jeudi matin seront consacrées à des journées spécifiquement Vérif. Les informations sur les exposés invités et contribués, l'inscription ainsi que l'organisation pratique des journées seront rogressivement complétées ci-dessous. Exposés invités David Baelde, IRISA, Ens Rennes, Proof-theoretical investigations into Squirrel & CCSA logics (slides) In this talk, I will give an overview of a particular logic-based methodology for proving security protocols, based on so-called CCSA logics and implemented in the Squirrel proof assistant, and I will more specifically present recent proof-theoretical results about a modal fragment of that logic. CCSA logics have been proposed by Bana and Comon in 2012 as a logic-based approach to reason about cryptographic protocols. Initially based in first-order logic and aimed for full automation, the core ideas of CCSA logics have been adapted to richer logical settings in a recent line of work. As a result, mechanized proofs of several protocols have been developed using the Squirrel proof assistant, which implements a rich, higher-order CCSA logic. One of the key ingredients in Squirrel's logic is the notion of "overwhelming truth". Cryptographers consider that asymptotic security holds when, for any possible attacker running in polynomial time, the probability that the attack succeeds is negligible, i.e. that it tends fast enough to zero with the size of secrets. In order to reason formally about cryptographic truth, one may thus consider logics where a formula is satisfied when it is true with overwhelming probability, i.e. a probability that tends fast enough to one with the size of secrets. Squirrel implements one such logic, but it relies on an ad-hoc proof system for overwhelming truth. To improve this situation, we have recently studied a propositional fragment of Squirrel's logic under the lens of modal logic. We first consider a modal logic of overwhelming truth, and show that it coincides with S5. In addition to providing an axiomatization, this brings a well-behaved proof system for our logic in the form of Poggiolesi’s hypersequent calculus. We then consider a logic that is closer to Squirrel’s language, where the overwhelming truth modality cannot be nested. In that case, we show that a simple proof system, based on regular sequents, is sound and complete. This result justifies the core of Squirrel’s proof system. Julie Cailler, LORIA, Université de Lorraine, SC-TPTP : étendre le format TPTP pour les preuves basées sur les séquents (slides) SC-TPTP est une extension du format TPTP (Thousands of Problems for Theorem Provers) conçue pour intégrer les preuves basées sur les séquents dans un cadre standardisé. En effet, ben qu'étant un standard dans la communauté de preuve automatique, le format SC-TPTP ne permet pas la représentation de preuves basées sur les séquents. Ces preuves sont pourtant très intéressantes, car elles se traduisent naturellement vers des assistants de preuve, permettant ainsi la génération de certificats de preuves. SC-TPTP remédie à cette limitation en ajoutant une expressivité supplémentaire au format, permettant de formaliser ces preuves tout en restant compatible avec les outils et formats existants. Le format est également conçu comme un format d’échange entre les prouveurs automatiques et interactifs. L’un des objectifs clés de SC-TPTP est de répondre à un besoin fondamental : éviter la prolifération des formats et des standards dans la communauté. En unifiant les représentations de preuves, SC-TPTP simplifie le développement d'outils de preuve, réduit la complexité des conversions entre formats et permet une adoption plus large de diverses approches de preuves. En parallèle, SC-TPTP s’accompagne d'une bibliothèque d'outils, SC-TPTP Utilities, incluant des prouveurs/assistants de preuve capables de générer/importer et valider des preuves au format SC-TPTP, ainsi que des outils de traduction permettant l’export vers d’autres systèmes de preuves interactifs comme Coq, facilitant ainsi encore plus l'interopérabilité. Arthur Charguéraud, INRIA, Interactive Program Verification using CFML (slides) The approach of verifying programs by means of an embedding Separation Logic in an interactive theorem prover has been developed over the past two decades. It has proved to be the tool of choice for the verification of data structures and algorithms with complex invariants. Moreover, work from last decade has shown how to generalize the approach for reasoning about concurrent programs, as well as for establishing time and space bounds. In this talk, I will give an overview of this state-of-the-art technology, focusing on sequential programs, and I present a demo of the CFML tool. Jean Goubault-Larrecq, LMF, ENS Paris-Saclay, Is there any trouble with the probabilistic powerdomain monad? (slides,associated webpage) In short, no. The origin of the trouble seems to be the title of a 1998 paper by A. Jung and R. Tix entitled "the troublesome probabilistic powerdomain". It seems that this has now come to be interpreted as justifying that one has to look beyond domain theory and dcpos to give semantics to higher-order probabilistic languages - and this interpretation is bogus. There is simply no problem giving semantics to such languages in terms of plain old dcpo semantics. Even classical theorems such as soundness and adequacy hold, a topic that I will touch only briefly. One issue, though, is that the classical probabilistic powerdomain monad is not known to be commutative. This is easily solved by replacing it by a variant. The simplest one is the monad of minimal valuations, but there are other choices, too. Although not all continuous valuations are minimal, enough of them are. This allows us to give semantics to a statistical programming language, with not just higher-order and probabilistic features, but also continuous distributions on exact real numbers (and soft conditioning: Lebesgue measure, and in fact any measure on the real numbers, induces a continuous valuation on the domain of exact reals that is in fact a minimal valuation. I will finish the presentation by giving a proof that there are dcpos on which not all continuous valuations are minimal; but this is hard to find, and not that simple to prove. Mickaël Randour, Université de Mons, Controllers in Reactive Synthesis: A Strategic Perspective In the game-theoretic approach toward controller synthesis, we model the interaction between a system to control and its environment as (some variation of) game between these entities, and we are looking for an appropriate (e.g., winning or optimal) strategy of the system. This strategy then constitutes a formal blueprint for a real-world controller for the system. The general consensus is that simple (e.g., using limited memory) strategies are better: corresponding controllers will be easier to conceive and understand, and cheaper to produce and maintain. This talk focuses on the complexity of strategies in a variety of synthesis contexts. We will discuss recent results regarding memory and randomness, and take a quick glance at what lies beyond our traditional ways of understanding the notion of complexity for strategies. Syvain Salvati, Cristal, Université de Lille, recognizability in functional programs (slides) We present an conservative extension of the notion of recognizability to simply typed lambda-calculus. This notion allows to solve syntactic problem in a general manner. We will present two examples: parsing in a very general setting and higher-order verification. Lina Ye, LMF, CentraleSupélec, Université Paris-Saclay, Decisiveness Analysis of Infinite (Dynamic) Probabilistic Models (slides) Decisiveness of infinite Markov chains with respect to some (finite or infinite) target set of states is a key property that allows to compute the reachability probability of this set up to an arbitrary precision. Most of the existing related works assume constant weights for defining the probability of a transition in the considered models. However numerous probabilistic modelings require (dynamic) weights that depend on both the current state and the transition. So we study and demonstrate that in the dynamic settings, the decisiveness is undecidable for both probabilistic one-counter machines and polynomial probabilistic Petri nets. Fortunately, we succeed to identify some interesting subclasses for which either the decisiveness is decidable in polynomial time or the models themselves are decisive with respect to a finite set. Inscriptions et propositions d'exposé Inscription L'inscription est gratuite mais obligatoire. Le formulaire d'inscription est ici: https://framaforms.org/journees-scalp-verif-novembre-2024-1726473230 La date limite pour l'inscription est fixée au 10 octobre Le formulaire d'inscription est pour toutes les rencontres, en commun avec Verif. Lors de l'inscription, vous serez invités à préciser à quelles demi-journées vous souhaitez participer. Vous serez également invités à dire si vous souhaitez proposer un exposé. Si vous souhaitez donner un exposé mais n'avez pas encore d'idée précise du sujet, vous pouvez laisser les champs vides et les envoyer par mail. Nous ne manquerons pas de vous recontacter pour récupérer les titres / abstracts manquants ! Toutes les thématiques du GT sont bienvenues, mais nous encourageons tout particulièrement les contributions à l'interface avec Verif. Propositions d'exposé La durée des exposés n'a pas encore été fixée, elle dépendra du nombre de propositions et des souhaits des orateurs/oratrices. Comme d'habitude, nous apprécions spécialement les contributions des jeunes (doctorant(e)s et post-doc) et demandons aux encadrant(e)s d'encourager leurs encadré(e)s à présenter leurs travaux. Nous invitons aussi les moins jeunes à venir assister aux journées, afin que les jeunes chercheurs puissent rencontrer la communauté Scalp. Informations pratiques Les rencontres se dérouleront à Lille. Elles sont organisées par des membres du laboratoire CRIStAL et se dérouleront dans les locaux de l'IRCICA: 50 avenue du Halley, 59650 Villeneuve d'Ascq, France. Depuis la gare Lille Flandres prendre la ligne de métro 1 vers 4 Cantons ce qui prend 15 minutes. L'IRCICA est à une quinzaine de minutes à pied de la station de métro: voir sur google map. Suggestions d'hôtels Nous suggérons de prendre des hôtels en centre ville, le quartier universitaire n'étant pas très animé. Quelques suggestions de restauration Près de la Grand Place: le Coq hardi la Houblonnière La Chicorée Les compagnons de la grappe Restaurant libanais: http://www.michelrestaurant.fr/ La rue de Gand dans le vieux Lille a plusieurs restaurants, par exemple: https://lafleurdelille-restaurant.fr/ Estaminet: https://www.chtitebrigitte.com/en/ Programme préliminaire Lundi après-midi 13h00-14h00 Accueil 14h00-15h00 Jean Goubault-Larrecq, Is there any trouble with the probabilistic powerdomain monad? (slides,associated webpage) 15h00-15h30 Leandro Gomes, Relational verification of probabilistic programs: an algebraic framework (slides) 15h30-16h00 Pause 16h00-16h30 Adrienne Lancelot, Interaction Equivalence (slides) 16h30-17h00 Jean-Baptiste Joinet, Multi-conclusion intuitionistic sequent calculi designed via ecumenical LL i.e. with a classical & an intuitionistic exponential 17h00-17h30 Anupam Das, Right linear lattices: an equational theory of alternating parity automata (slides) 17h30-18h00 Adrien Ragot, Parsing Correctness Criterion for Second Order Multiplicative Linear Logic (slides) Mardi matin 9h00 - 10h00 Julie Cailler, SC-TPTP : étendre le format TPTP pour les preuves basées sur les séquents (slides) 10h00 - 10h30 Abhishek De, Bounded Henkin Quantifiers and the Exponential Time Hierarchy (slides) 10h30 - 11h00 Pause 11h00 - 11h30 Simon Mirwasser, Graded differential linear logic: can we go higher-order? (slides) 11h30 - 12h00 Kostia Chardonnet, Le Many-worlds calculus 12h00 - 12h30 Loic Pujet, Strictifying Categories with Families (slides) Mardi après-midi 14h00 - 15h00 David Baelde, Proof-theoretical investigations into Squirrel & CCSA logics (slides) 15h00 - 15h30 Tito Nguyen, Higher-order model checking meets implicit automata (slides) 15h30 - 16h00 Pause 16h00 - 16h30 Victor Sannier, Types de session pour la composition concurrente de la confidentialité différentielle interactive (slides) 16h30 - 17h00 Stéphane Aubry, Vers une preuve automatique de l'algorithme concurrent CNDFS (slides) 17h00 - 17h30 Benjamin Lion, Stateful Synchronous Dataflow: Harnessing Distributive Laws of a Comonad over a Monad (slides) 17h30 - 19h00 Discussions Mercredi matin 9h00 - 10h00 Sylvain Salvati, Recognisability in functional programs (slides) 10h00 - 10h30 Isa Vialard, Measuring well quasi-orders (slides) 10h30 - 11h00 Pause 11h00 - 11h30 Laetitia Laversa, Execution-time opacity control for timed automata (slides) 11h30 - 12h00 Gaëtan Staquet, Active Learning of Mealy Machines with Timers (slides) 12h00 - 12h30 Emily Clément, Higher Dimensional (Timed) Automata (slides) Mercredi après-midi 14h00 - 15h00 Lina Ye, Decisiveness Analysis of Infinite (Dynamic) Probabilistic Models (slides) 15h00 - 15h30 Pierre Vandenhove, Revelations: A Decidable Class of POMDPs with Omega-Regular Objectives (slides) 15h30 - 16h00 Pause 16h00 - 17h00 Arthur Charguéraud, Interactive Program Verification using CFML (slides) 17h00 - 17h30 James Main, Verifying Concisely Represented Strategies in One-Counter Markov Decision Processes (slides) 17h30 - 18h00 Chloé Capon, Taming Large MDPs Through Stochastic Games (slides) Jeudi matin 9h00 - 10h00 Mickael Randour, Controllers in Reactive Synthesis: A Strategic Perspective 10h00 - 10h30 Dylan Bellier, A game-theoretic interpretation of Boolean operators in Strategic Reasoning (slides) 10h30 - 11h00 Pause 11h00 - 11h30 Olivier Idir, A game characterization of the parity index of regular tree languages (slides) 11h30 - 12h00 Romain Delpy, An automata-based approach for synchronizable mailbox communication 12h00 - 12h30 Lucie Guillou, Reachability in Wait-Only Broadcast Networks (slides) Liste des exposés contribués Stéphane Aubry, USPN-LIPN, Vers une preuve automatique de l'algorithme concurrent CNDFS L'algorithme CNDFS (Concurrent Nested Depth First Search) est une version concurrente de l'algorithme NDFS utilisé en Model Checking pour vérifier les propriétés de logique temporelle. Celui-ci repose sur la recherche de cycles dans un graphe orienté. Notre objectif est de le prouver formellement, à l'aide d'outils de vérification automatique tels que, par exemple, Vercors ou F*. Il s'agit d'un travail en cours, où nous commençons par la version séquentielle de l'algorithme, afin d'explorer les avantages et inconvénients des différentes approches de ces outils. David Baelde, ENS Rennes, Proof-theoretical investigations into Squirrel & CCSA logics (slides) In this talk, I will give an overview of a particular logic-based methodology for proving security protocols, based on so-called CCSA logics and implemented in the Squirrel proof assistant, and I will more specifically present recent proof-theoretical results about a modal fragment of that logic. CCSA logics have been proposed by Bana and Comon in 2012 as a logic-based approach to reason about cryptographic protocols. Initially based in first-order logic and aimed for full automation, the core ideas of CCSA logics have been adapted to richer logical settings in a recent line of work. As a result, mechanized proofs of several protocols have been developed using the Squirrel proof assistant, which implements a rich, higher-order CCSA logic. One of the key ingredients in Squirrel's logic is the notion of “overwhelming truth”. Cryptographers consider that asymptotic security holds when, for any possible attacker running in polynomial time, the probability that the attack succeeds is negligible, i.e. that it tends fast enough to zero with the size of secrets. In order to reason formally about cryptographic truth, one may thus consider logics where a formula is satisfied when it is true with overwhelming probability, i.e. a probability that tends fast enough to one with the size of secrets. Squirrel implements one such logic, but it relies on an ad-hoc proof system for overwhelming truth. To improve this situation, we have recently studied a propositional fragment of Squirrel's logic under the lens of modal logic. We first consider a modal logic of overwhelming truth, and show that it coincides with S5. In addition to providing an axiomatization, this brings a well-behaved proof system for our logic in the form of Poggiolesi’s hypersequent calculus. We then consider a logic that is closer to Squirrel’s language, where the overwhelming truth modality cannot be nested. In that case, we show that a simple proof system, based on regular sequents, is sound and complete. This result justifies the core of Squirrel’s proof system. Dylan Bellier, Univ Rennes, A game-theoretic interpretation of Boolean operators in Strategic Reasoning Strategy logic (SL) has two major flaws. First, the assoiated decision problems have a high complexity: model checking is non elementary and satisfiability is undecidable. The quantified strategies might not be realizable. However, these flaws appear to be related: for the One-Goal fragment, decision problems have a 2-EXPTIME complexity and quantifying over realizable strategies suffices. In this work, we propose an approach to define a game-theoretic semantics for the Conjunctive-Goal/Disjunctive-Goal fragments of SL that enforce realizability of strategies. This semantics game casts Boolean operators as players whose actions reflect their on-the-fly-choice of which conjunct/disjunct to verify. Julie Cailler, LORIA, Université de Lorraine, SC-TPTP : étendre le format TPTP pour les preuves basées sur les séquents (slides) SC-TPTP est une extension du format TPTP (Thousands of Problems for Theorem Provers) conçue pour intégrer les preuves basées sur les séquents dans un cadre standardisé. En effet, ben qu'étant un standard dans la communauté de preuve automatique, le format SC-TPTP ne permet pas la représentation de preuves basées sur les séquents. Ces preuves sont pourtant très intéressantes, car elles se traduisent naturellement vers des assistants de preuve, permettant ainsi la génération de certificats de preuves. SC-TPTP remédie à cette limitation en ajoutant une expressivité supplémentaire au format, permettant de formaliser ces preuves tout en restant compatible avec les outils et formats existants. Le format est également conçu comme un format d’échange entre les prouveurs automatiques et interactifs. L’un des objectifs clés de SC-TPTP est de répondre à un besoin fondamental : éviter la prolifération des formats et des standards dans la communauté. En unifiant les représentations de preuves, SC-TPTP simplifie le développement d'outils de preuve, réduit la complexité des conversions entre formats et permet une adoption plus large de diverses approches de preuves. En parallèle, SC-TPTP s’accompagne d'une bibliothèque d'outils, SC-TPTP Utilities, incluant des prouveurs/assistants de preuve capables de générer/importer et valider des preuves au format SC-TPTP, ainsi que des outils de traduction permettant l’export vers d’autres systèmes de preuves interactifs comme Coq, facilitant ainsi encore plus l'interopérabilité. Chloé Capon, Université de Mons (UMONS), Taming Large MDPs Through Stochastic Games Markov decision processes (MDPs) are widely used to model systems with both probabilistic and nondeterministic behavior. While probabilistic model checking is effective for verifying these models, the state-space explosion problem constitutes a major challenge. To address this, abstraction-refinement techniques create smaller, simpler models by excluding irrelevant parts. This work extends the framework from [1] to handle MDPs with multiple reachability objectives, using stochastic two-player games for the abstractions. By distinguishing the nondeterminism from the original MDP and the one from the abstraction process, we compute upper and lower bounds for the Pareto frontiers. These bounds provide a measure of the abstraction's quality and serves as the foundation for the refinement method that we introduce. This is based on joint work with Nicolas Lecomte, Mickael Randour and Petr Novotný. [1] M. Kattenbelt, M. Kwiatkowska, G. Norman and D. Parker, A game-based abstraction-refinement framework for Markov decision processes, FMSD, 2010. Arthur Charguéraud, INRIA, Interactive Program Verification using CFML The approach of verifying programs by means of an embedding Separation Logic in an interactive theorem prover has been developed over the past two decades. It has proved to be the tool of choice for the verification of data structures and algorithms with complex invariants. Moreover, work from last decade has shown how to generalize the approach for reasoning about concurrent programs, as well as for establishing time and space bounds. In this talk, I will give an overview of this state-of-the-art technology, focusing on sequential programs, and I present a demo of the CFML tool. Kostia Chardonnet, Inria Nancy, Le Many-Worlds Calculus Nous explorons l'interaction entre deux structures monoïdales : une multiplicative, pour représenter des paires et une additive pour représenter des choix d'exécutions. Nous proposons une PROP pour modéliser le calcul dans ce cadre. Notre modèle est paramétré par une structure algébrique. Ainsi, le modèle permet de représenter le calcul classique, non-déterministe, probabiliste, ou quantique, selon le choix de la structure algébrique choisie. Emily Clement, CNRS, LIPN UMR 7030, Université Sorbonne Paris Nord, F-93430 Villetaneuse, France, Higher Dimensional (Timed) Automata Temporal logics are a powerful tool to specify properties of computational systems. For concurrent programs, Higher Dimensional Automata (HDA) are a very expressive model of non-interleaving concurrency. HDA recognize languages of partially ordered multisets, or pomsets. Recent work has shown that Monadic Second Order (MSO) logic is as expressive as HDA for pomset languages. In this paper, we investigate the class of pomset languages that are definable in First Order (FO) logic. In the case of words, Kamp's theorem states that FO is as expressive as Linear Temporal Logic (LTL). Our aim is to prove a variant of Kamp's theorem for pomset languages. Thus, we define a temporal logic called Sparse Pomset Temporal Logic (SPTL), and show that it is equivalent to FO, when there is no autoconcurrency. Our future goal is also to study timed temporal logics on HDTA, Higher Dimension Timed Automata. Anupam Das, University of Birmingham, Right-linear lattices: an equational theory of alternating parity automata We consider a syntax for omega-regular languages over lattices with fixed points. The resulting algebraic structures, right-linear lattices (RLLs), 'dualise' ones from previous work, right-linear algebras (RLAs). A key distinction of our approach is that there is no multiplicative structure on RLLs or RLAs, unlike Kleene algebras (and friends); indeed their syntax is just a notation for alternating parity automata over omega-words. Our main results are a sound and complete cyclic system and axiomatisation, with respect to the intended language model. This is joint work with Abhishek De. Abhishek De, University of Birmingham, Bounded Henkin Quantifiers and the Exponential Time Hierarchy In logic, quantifiers typically have an implicit linear order of dependencies. Henkin introduced a more general framework for quantifier prefixes, allowing for partial orderings among quantifiers. These quantifiers, now known as Henkin quantifiers, have been extensively studied in logic and have found significant applications in linguistics, arithmetic, and descriptive complexity. Surprisingly, bounded versions of Henkin quantifiers, which restrict the range of these quantifiers, have not been explored. This paper defines bounded Henkin quantifiers and examines their properties from a complexity-theoretic perspective. In particular, we show that the set of predicates definable by quantifier-free formulas prefixed by a bounded Henkin quantifier is exactly NEXP. The proof goes via machine models defined using bounded Henkin quantifiers. Finally, we show that formulas with Henkin quantifiers define a complexity class contained in Delta_2 in the exponential hierarchy and define a natural complete problem for this class. Romain DELPY, Université de Bordeaux, LaBRI, An automata-based approach for synchronizable mailbox communication We revisit finite-state communicating systems with round-based communication under mailbox semantics. Mailboxes correspond to one FIFO buffer per process (instead of one buffer per pair of processes in peer-to-peer systems). Round-based communication corresponds to sequences of rounds in which processes can first send messages, then only receive (and receives must be in the same round as their sends). A system is called synchronizable if every execution can be re-scheduled into an equivalent execution that is a sequence of rounds. We know from previous results that reachability is PSPACE-complete for synchronizable systems. In this talk we show that we can check if a mailbox system is synchronizable thanks to a novel automata-based approach. From this we get that checking synchronizability is PSPACE-complete. The same question is undecidable under peer-to-peer semantics. We also show that model-checking synchronizable systems for a natural subclass of regular properties is a PSPACE-complete problem. Joint work with Anca Muscholl & Grégoire Sutre Leandro Gomes, CRIStAL & Université de Lille, Relational verification of probabilistic programs: an algebraic framework This presentation introduces a framework devoted to formal reasoning on relational properties of probabilistic imperative programs. Relational properties are properties which relate the execution of two programs (possibly the same one) on two initial memories. We aim at extending the algebraic approach of Kleene Algebras with Tests (KAT) to relational properties of probabilistic programs. For that we consider the approach of Guarded Kleene Algebras with Tests (GKAT), which can be used for representing probabilistic programs, and define a relational version of it, called Bi-guarded Kleene Algebras with Tests (BiGKAT) together with a semantics. We show that the setting of BiGKAT is expressive enough to encode a finitary version of probabilistic Relational Hoare Logic (pRHL) (without the While rule), a program logic that has been introduced in the literature for the verification of relational properties of probabilistic programs. We also discuss the additional expressivity brought by BiGKAT. Jean Goubault-Larrecq, Is there any trouble with the probabilistic powerdomain monad? In short, no. The origin of the trouble seems to be the title of a 1998 paper by A. Jung and R. Tix entitled “the troublesome probabilistic powerdomain”. It seems that this has now come to be interpreted as justifying that one has to look beyond domain theory and dcpos to give semantics to higher-order probabilistic languages - and this interpretation is bogus. There is simply no problem giving semantics to such languages in terms of plain old dcpo semantics. Even classical theorems such as soundness and adequacy hold, a topic that I will touch only briefly. One issue, though, is that the classical probabilistic powerdomain monad is not known to be commutative. This is easily solved by replacing it by a variant. The simplest one is the monad of minimal valuations, but there are other choices, too. Although not all continuous valuations are minimal, enough of them are. This allows us to give semantics to a statistical programming language, with not just higher-order and probabilistic features, but also continuous distributions on exact real numbers (and soft conditioning: Lebesgue measure, and in fact any measure on the real numbers, induces a continuous valuation on the domain of exact reals that is in fact a minimal valuation. I will finish the presentation by giving a proof that there are dcpos on which not all continuous valuations are minimal; but this is hard to find, and not that simple to prove. Lucie Guillou, IRIF, Reachability in Wait-Only Broadcast Networks In this ongoing work, we investigate networks composed of an unbounded number of agents that communicate via broadcasts. All agents execute the same protocol, described as a finite-state machine. The reachability problem asks whether, given a protocol and a target state, there exists a number of agents and a sequence of actions that leads to a configuration where all agents are in the specified target state. This problem is known to be undecidable in the general case. However, we focus on Wait-Only protocols, where no state allows an agent to both broadcast and receive messages. Under this restriction, we show that the reachability problem becomes decidable, though it is as hard as the reachability problem for Petri nets. Olivier Idir, IRIF, A game characterization of the parity index of regular tree languages Modal mu-calculus is equivalent to parity automata on infinite trees. The minimal number of priorities required by some tree automaton to recognize a regular tree language then corresponds to the fixpoint alternation depth required in the corresponding formula. However, deciding this index is a long-standing problem. In their 2008 paper, Colcombet and Löding reduced this problem to a boundedness question on distance-parity automata. This proof used complex machinery which makes it less accessible than ideal, and uses the less standard model of distance parity automata. In this joint work with Karoliina Lehtinen, we revisit this result, and propose a simplified proof. We combined tools developed by Lehtinen to solve parity games in quasi-polynomial time, and hierarchical counters as used by Colcombet and Löding. We hope to use this result to relate the parity index problem with the theory of universal trees, as developed to solve parity games. Jean-Baptiste Joinet, IRPhiL Université Jean Moulin Lyon 3, Multi-conclusion intuitionistic sequent calculi designed via ecumenical LL i.e. with a classical & an intuitionistic exponential “Logical Ecumenism’’ (a terminology introduced by Dag Prawitz) aims at distinguishing Intuitionistic and Classical Logic not only at the level of rules, but also at the level of connectives themselves : typically by introducing two implications, a classical one and an intuitionistic one, each of them being endowed with specific rules. Linear Logic approaches that question in a different way. When one interprets “intuitionistic'” and “classical” connectives, e.g. implication, in Linear Logic, their difference is not caught at the level of the implication connective itself (the linear implication remains the sole implication connective used), but by our ability to use in specific ways the modalities of Linear Logic (! and ?) when interpreting implicative formulas. Typically, the “?” exponential is not needed in order to interpret standard intuitionistic implicative sequent calculus $\mathsf{LJ}$, since that modality indicates the (potential) use of right structural rules – rules which are not present in $\mathsf{LJ}$. In the present talk, I will address the question of how Linear Logic is able to distinguish intuitionistic and classical implications, when one considers multiconclusions formulation of intuitionistic logic (where right structural rules are allowed). In order to investigate that question, I will introduce a variant of sequent calculus for Linear logic equipped with one interrogation mark but two exclamation marks – one symmetrical, one dissymetrical – all those exponentials leaving harmoniously together (cf. my contributed “Dissymetrical Linear Logics” in TLLA-LINEARITY-2022, where I designed a bunch of systems for logics beeing intermediary, at the level of provability, between Intuitionistic and Classical Linear Logic). My aim is show how those ecumenical exponentials may be used as a tool to design multi-conclusions Intuitionistic sequent calculi. Adrienne Lancelot, INRIA & LIX, Ecole Polytechnique and IRIF, CNRS, Université Paris Cité, Interaction Equivalence Contextual equivalence is the de facto standard notion of program equivalence. A key theorem is that contextual equivalence is an equational theory. Making contextual equivalence more intensional, for example taking into account the time cost of the computation, seems a natural refinement. Such a change, however, does not induce an equational theory, for an apparently essential reason: cost is not invariant under reduction. In the paradigmatic case of the untyped λ-calculus, we introduce interaction equivalence. Inspired by game semantics, we observe the number of interaction steps between terms and contexts but—crucially—ignore their own internal steps. We prove that interaction equivalence is an equational theory and we characterize it as B, the well-known theory induced by Böhm tree equality. Ours is the first observational characterization of B obtained without enriching the discriminating power of contexts with extra features such as non-determinism. To prove our results, we develop interaction-based refinements of the Böhm-out technique and of intersection types. Laetitia Laversa, IRIF, Université Paris Cité, Execution-time opacity control for timed automata Timing leaks in timed automata (TA) can occur whenever an attacker is able to deduce a secret by observing some timed behavior. In execution-time opacity, the attacker aims at deducing whether a private location was visited, by observing only the execution time. It can be decided whether a TA is opaque in this setting. In this work, we tackle control, and show that we are able to decide whether a TA can be controlled at runtime to ensure opacity. Our method is constructive, in the sense that we can exhibit such a controller. We also address the case when the attacker cannot have an infinite precision in its observations. Benjamin Lion, Inria Rennes, Stateful Synchronous Dataflow: Harnessing Distributive Laws of a Comonad over a Monad We introduce a formal language specifically designed for stateful synchronous dataflow programming. Our language extends the set of standard functional dataflow primitives with stateful operations on memory. We make use of a comonad to encode the dataflow nature of programs and of a monad to capture the effects during execution. The compositionality of the semantics is ensured by proving a new distributive law of the comonad over the monad. We provide illustrative examples to clarify key concepts and demonstrate the application of our formal framework in proving fundamental properties of stateful dataflow programs using Coq. James Main, F.R.S.-FNRS & Université de Mons (UMONS), Verifying Concisely Represented Strategies in One-Counter Markov Decision Processes Markov decision processes (MDPs) model reactive systems that continuously interact with a stochastic environment. To model resource usage along executions of systems, an MDP can be augmented with a counter keeping track of the resource level. This extension is called a one-counter MDP (OC-MDP). OC-MDPs induce infinite-state MDPs whose configurations are given by states of the MDP and natural counter values. We consider a special class of strategies on these infinite-state MDPs, called interval strategies. A strategy is an interval strategy if it is memoryless (i.e., its decisions depend only on the current state and counter value) and there exist finitely many intervals partitioning the natural numbers such that all decisions taken in a state for two counter values within the same interval coincide. In general, no upper bound is required on counter values, thus interval strategies are infinite objects that admit a finite representation. We propose verification algorithms for OC-MDPs and interval strategies. We consider two objectives: state reachability and termination. The latter objective is the set of executions such that counter value zero is reached for the first time in a state within a designated set of targets. We provide a polynomial space algorithm for the interval strategy verification problem and square-root-sum lower bounds. This talk is based on joint work with Michal Ajdarów (Masaryk University), Petr Novotný (Masaryk University) and Mickael Randour (F.R.S.-FNRS & Université de Mons). Simon Mirwasser, LIPN, USPN, Graded differential linear logic: can we go higher-order? Differential linear logic gives a framework to interpret linear and smooth maps between vector spaces, together with the differential of a map. One can extend this framework in order to interpret partial differential equations as well. This is done by indexing the exponential connectives of differential linear logic by elements of a semiring (a technique known as grading), and by studying the particular case with a semiring of partial differential operators. However, many issues appear when one tries to add higher-order to this graded extension, both from the syntax and the semantics. We present these issues here, and give some solutions to both of them. This is work in progress with Marie Kerjean. Tito Nguyen, LIS, Higher-order model checking meets implicit automata Higher-order model checking (HOMC) is an approach to verification of functional programs, based on checking monadic second-order properties of trees generated by typed λ-calculus with recursion. We slightly extend some tools developed by Grellois and Melliès for HOMC — a finitary colored Scott semantics (or equivalently, idempotent intersection type system) for infinitary λ-terms — in order to give a new characterisation of ω-regular languages of infinite words. Joint work with Abhishek De, Charles Grellois and Cécilia Pradic. Loïc Pujet, Université de Stockholm, Strictifying Categories with Families Categories with families (CwF) are perhaps the most widely used notion of models for dependent types. They can be described by an algebraic signature with dependent sorts for contexts, substitutions, types and terms, as well as a plethora of constants and equations. Unfortunately, this mix of dependent sorts and equations is particularly prone to transport hell, and in practice it is nearly impossible to prove non-trivial results using CwFs in a proof assistant. In this talk, I will present a method based on Pédrot's “prefascist sets” to strictify (nearly) all the equations of a CwF, so that they hold by definition. I will then discuss applications of this method to formal proofs of canonicity and normalisation. This is joint work with Ambrus Kaposi. Adrien Ragot, Université Sorbonne Paris Nord - Universita degli studi Roma Tre, Parsing Correctness Criterion for Second Order Multiplicative Linear Logic We introduce a method for defining a Parsing Correctness Criterion for Second-Order Multiplicative Linear Logic proof structures, where bounded variables are represented using pointers. A key insight in demonstrating the validity of this criterion is recognizing that a parsing sequence involving pointers can be viewed as a standard parsing sequence (without pointers), where a 'forall' link is contracted only if the 'exists' link it depends on has already been contracted. This illustrates how pointers store part of the sequentiality information, ensuring that 'exists' links are introduced before the corresponding 'forall' links. Moreover, the criterion is able to construct a sequent calculus proof from a parsing sequence, and because the parsing is confluent rewriting on proof nets and always decrease the size of a net the criterion runs in quadratic time. Mickael Randour, Université de Mons, Controllers in Reactive Synthesis: A Strategic Perspective In the game-theoretic approach toward controller synthesis, we model the interaction between a system to control and its environment as (some variation of) game between these entities, and we are looking for an appropriate (e.g., winning or optimal) strategy of the system. This strategy then constitutes a formal blueprint for a real-world controller for the system. The general consensus is that simple (e.g., using limited memory) strategies are better: corresponding controllers will be easier to conceive and understand, and cheaper to produce and maintain. This talk focuses on the complexity of strategies in a variety of synthesis contexts. We will discuss recent results regarding memory and randomness, and take a quick glance at what lies beyond our traditional ways of understanding the notion of complexity for strategies. Syvain Salvati, Cristal, Université de Lille, recognizability in functional programs (slides) We present an conservative extension of the notion of recognizability to simply typed lambda-calculus. This notion allows to solve syntactic problem in a general manner. We will present two examples: parsing in a very general setting and higher-order verification. Victor Sannier, Laboratoire CRIStAL, Université de Lille, Types de session pour la composition concurrente de la confidentialité différentielle interactive TBA Gaëtan Staquet, Inria, Active Learning of Mealy Machines with Timers In order to understand and verify complex systems, we need accurate models that are either understandable for humans or can be analyzed fully automatically. Such models, however, are typically not available for legacy software. Active automata learning is a black-box technique for constructing state machine models of software and hardware components from information obtained through testing (i.e., providing inputs and observing the resulting outputs) and may thus fill this gap. In many applications, timing plays a crucial role, which in turn makes extending automata learning to a setting that incorporates quantitative timing information challenging. In this talk, we present an active learning algorithm for a general class of Mealy machines with timers (MMTs) in a black-box context. A Mealy machine is a finite state machine that outputs a sequence of symbols for every processed input word. We then augment it with timers that force certain transitions to occur after a certain amount of time has elapsed. Our algorithm is an extension of the L# algorithm of Vaandrager et al. [1] to a timed setting. Like the algorithm for learning timed automata proposed by Waga [2], our algorithm is inspired by ideas of Maler & Pnueli [3]. Based on the elementary languages of [3], both Waga's and our algorithm use symbolic queries, which are then implemented using finitely many concrete queries. However, whereas Waga needs exponentially many concrete queries to implement a single symbolic query, we only need a polynomial number. This is because in order to learn a timed automaton, a learner needs to determine the exact guard and reset for each transition (out of exponentially many possibilities), whereas for learning an MMT a learner only needs to figure out which of the preceding transitions caused a timeout. As shown in a previous work [4], this can be done efficiently for a subclass of MMTs that are “race-avoiding”: if a timeout is caused by a preceding input then a slight change in the timing of this input will induce a corresponding change in the timing of the timeout. [1]: Frits W. Vaandrager, Bharat Garhewal, Jurriaan Rot, and Thorsten Wißmann. A new approach for active automata learning based on apartness. TACAS 2022. [2]: Masaki Waga. Active learning of deterministic timed automata with myhill-nerode style characterization. CAV 2023. [3]: Oded Maler and Amir Pnueli. On recognizable timed languages. FOSSACS 2004. [4]: Véronique Bruyère, Guillermo A. Pérez, Gaëtan Staquet, and Frits W. Vaandrager. Automata with timers. FORMATS 2023. Pierre Vandenhove, Université de Mons, Revelations: A Decidable Class of POMDPs with Omega-Regular Objectives Partially observable Markov decision processes (POMDPs) form a prominent model for uncertainty in sequential decision making. We are interested in constructing algorithms with theoretical guarantees to determine whether the agent has a strategy ensuring a given specification with probability 1. This well-studied problem is known to be undecidable already for very simple omega-regular objectives, because of the difficulty of reasoning on uncertain events. We introduce a revelation mechanism which restricts information loss by requiring that, almost surely, the agent has eventually full information of the current state. Our main technical results are to construct exact algorithms for two classes of POMDPs called weakly and strongly revealing. Importantly, the decidable cases reduce to the analysis of a finite belief-support Markov decision process. This yields a conceptually simple and exact algorithm for a large class of POMDPs. Isa Vialard, Max Plank Institute for Software Systems, Measuring well quasi-orders Well quasi orderings (WQOs) are at the heart of the theory of Well-Structured Systems (WSTS), a class of computational models that brought numerous important advances for the automatic verification of infinite-state systems. Recent developments in this field links the complexity of WQO-based algorithms to ordinal measures of WQOs : the maximal order type, ordinal height and ordinal width. One main challenge is to compute the ordinal invariants of complex well quasi-orders built from simpler well quasi-orders through classical operation, such as the Cartesian product, and high-order constructions, like the finite words embedding. In my thesis, I computed compositionally the maximal order type of the direct product, the width of the multiset embedding, and the height and width of the multiset ordering. Furthermore, I compute the width of the Cartesian product in restricted cases and studied the ordinal measures of the finite powerset.In the process, I developed several tools and techniques, notably a game-theoretical approach to computing width using the notion of quasi-incomparable families of subsets. To tackle the width of the multiset ordering, I introduced and studied a fourth ordinal invariant, the friendly order type. Lina Ye, LMF, CentraleSupélec, Université Paris-Saclay, Decisiveness Analysis of Infinite (Dynamic) Probabilistic Models Decisiveness of infinite Markov chains with respect to some (finite or infinite) target set of states is a key property that allows to compute the reachability probability of this set up to an arbitrary precision. Most of the existing related works assume constant weights for defining the probability of a transition in the considered models. However numerous probabilistic modelings require (dynamic) weights that depend on both the current state and the transition. So we study and demonstrate that in the dynamic settings, the decisiveness is undecidable for both probabilistic one-counter machines and polynomial probabilistic Petri nets. Fortunately, we succeed to identify some interesting subclasses for which either the decisiveness is decidable in polynomial time or the models themselves are decisive with respect to a finite set. Participants Aubry Stéphane Baelde David Baillot Patrick Bellier Dylan Bertrand Nathalie Blanchi Victor Bliudze Simon Breuvart Flavien Cailler Julie Capon Chloé Cerda Rémy Chardonnet Kostia Clairambault Pierre Clement Emily Das Anupam DE Abhishek DELPY Romain Evangelista Sami Fievet Baptiste FOREST Simon Goeminne Aline Gomes Leandro Goubault-Larrecq Jean Goutagny Pierre Grandmont Christophe Guillou Lucie Harington Elies Idir Idir Joinet Jean-Baptiste Keller Chantal Kerinec Axel Koleilat Jad Lancelot Adrienne Lani Luca Laure Thomas Laversa Laetitia Lion Benjamin Maestracci Valentin Main James Marin Sonia Marinho Dylan Mayero Micaela Mirwasser Simon Monat Raphaël Munch-Maccagnoni Guillaume Nowak David Nguyễn Lê Thành Dũng (Tito) Ortiz James PECHOUX Romain Pinchinat Sophie Pujet Loïc Ragot Adrien Randour Mickael Rima Amélie Rusu Vlad Saurin Alexis Salvati Sylvain Sannier Victor Schlehuber-Caissier Philipp Staquet Gaëtan Vandenhove Pierre Vialard Isa Walch Aymeric Ye Lina Comité d'organisation Comité d'organisation des rencontres conjointes Scalp-Vérif: Nathalie Bertrand (Verif) Pierre Clairambault (Scalp) Chantal Keller (Scalp) David Nowak (Cristal) Pierre-Alain Reynier (Verif) Vlad Rusu (Cristal) Alexis Saurin (Scalp)