~~NOCACHE~~ /* DO NOT EDIT THIS FILE */ [[en:seminaires:verif:index|Verification]]\\ Friday November 29, 2024, 11AM, 3052 and [[https://u-paris.zoom.us/j/87460234504?pwd=mVUPogiquRZpL0HxEVffccgKRTZ1ID.1|Zoom link]]\\ **Raya Elsaleh** (Hebrew University of Jerusalem) //The Road to Improving Neural Network Verifiers// \\ Deep neural networks are becoming key components in diverse systems, but these systems often function as "black boxes," making it difficult to verify their correctness. This opacity is particularly concerning for safety-critical applications like autonomous vehicles, where reliability is essential. Recent advances in neural network verification aim to address these challenges by formally analyzing network behavior. However, verification remains challenging, particularly due to scalability issues and the complexity of DNN verifiers, which can themselves be prone to errors. In this talk, I will review recent developments in neural network verification approaches. Additionally, I will introduce a delta-debugging technique designed to minimize inputs that trigger bugs in the verifiers by reducing network size, thereby streamlining the debugging process for more reliable outcomes. [[en:seminaires:verif:index|Verification]]\\ Monday November 25, 2024, 11AM, 3052 and [[https://u-paris.zoom.us/j/87460234504?pwd=mVUPogiquRZpL0HxEVffccgKRTZ1ID.1|Zoom link]]\\ **Laetitia Laversa** (IRIF) //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 the work presented in this talk, 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 sens that we can exhibit such a controller. [[en:seminaires:verif:index|Verification]]\\ Monday November 18, 2024, 11AM, 3052 and [[https://u-paris.zoom.us/j/87460234504?pwd=mVUPogiquRZpL0HxEVffccgKRTZ1ID.1|Zoom link]]\\ **Romain Delpy** (LaBRI, Univ. Bordeaux) //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. [[en:seminaires:verif:index|Verification]]\\ Friday October 4, 2024, 11AM, 3052 and [[https://u-paris.zoom.us/j/89886269671?pwd=QlgvOVBmdjZTVGZqamdOWVdSWWU5UT09|Zoom link]]\\ **Eric Koskinen** (Stevens Institute of Technology) //Inferring Accumulative Effects of Higher Order Programs// \\ Many temporal safety properties of higher-order programs go beyond simple event sequencing and require an automaton register (or "accumulator") to express, such as input-dependency, event summation, resource usage, ensuring equal event magnitude, computation cost, etc. Some steps have been made towards verifying more basic temporal event sequences via reductions to fair termination [Murase et al. 2016] or some input-dependent properties through deductive proof systems [Nanjo et al. 2018]. However, there are currently no automated techniques to verify the more general class of register-automaton safety properties of higher-order programs. We introduce an abstract interpretation-based analysis to compute dependent, register-automata effects of recursive, higher-order programs. We capture properties of a program’s effects in terms of automata that summarizes the history of observed effects using an accumulator register. The key novelty is a new abstract domain for context-dependent effects, capable of abstracting relations between the program environment, the automaton control state, and the accumulator value. The upshot is a dataflow type and effect system that computes context-sensitive effect summaries. We demonstrate our work via a prototype implementation that computes dependent effect summaries (and validates assertions) for OCaml-like recursive higher order programs. As a basis of comparison, we describe reductions to assertion checking for effect-free programs, and demonstrate that our approach outperforms prior tools Drift, MoCHi and RCaml/PCSat. [[en:seminaires:verif:index|Verification]]\\ Monday September 30, 2024, 11AM, 3052 and [[https://u-paris.zoom.us/j/89886269671?pwd=QlgvOVBmdjZTVGZqamdOWVdSWWU5UT09|Zoom link]]\\ **Catalin Dima** (Université Paris-Est Créteil Val de Marne) //Rational synthesis in the commons (based on joint work with Rodica Bozianu, Youssouf Oualhadj and Nicolas Troquard)// \\ Turn-based games on graphs are games where the states are controlled by one and only one player who decides which edge to follow. Each player has a temporal objective that he tries to achieve. One player is the designated ‘controller’, whose objective captures the desirable outcomes of the whole system. Cooperative rational synthesis is the problem of computing a Nash equilibrium that satisfies the controller’s objective, while non-cooperative rational synthesis is the task of automatically constructing a controller that ensures the satisfaction of controller's objective against any Nash equilibrium involving the rest of the agents. We extend this setting to a context in which agents have access to common pool resources, represented as non-negative numbers. We consider two types of agents: careless and careful. Careless agents only care for their temporal objective, while careful agents also pay attention not to deplete the system’s resources. We solve the problems of cooperative and non-cooperative rational synthesis in such games involving a single resource, for parity objectives and objectives given by LTL formulas. The results are based on encodings into two-player energy parity games. [[en:seminaires:verif:index|Verification]]\\ Monday June 17, 2024, 11AM, 4071 and [[https://u-paris.zoom.us/j/89886269671?pwd=QlgvOVBmdjZTVGZqamdOWVdSWWU5UT09|Zoom link]]\\ **Shibashis Guha** (TIFR Mumbai) //Strategy synthesis for global window PCTL// \\ Given a Markov decision process (MDP) M and a formula Phi, the strategy synthesis problem asks if there exists a strategy sigma such that the resulting Markov chain M[sigma] satisfies Phi. This problem is known to be undecidable for the probabilistic temporal logic PCTL. We study a class of formulae that can be seen as a fragment of PCTL where a local, bounded horizon property is enforced all along an execution. Moreover, we allow for linear expressions in the probabilistic inequalities. This logic is at the frontier of decidability, depending on the type of strategies considered. In particular, strategy synthesis is shown to be decidable when strategies are deterministic while the problem is undecidable for arbitrary strategies. Joint work with Benjamin Bordais, Damien Busatto-Gaston, and Jean-François Raskin [[en:seminaires:verif:index|Verification]]\\ Monday May 27, 2024, 11AM, 3052 and [[https://u-paris.zoom.us/j/89886269671?pwd=QlgvOVBmdjZTVGZqamdOWVdSWWU5UT09|Zoom link]]\\ **Nicolas Amat** (IMDEA) //A polyhedral Framework for Reachability Problems in Petri Nets// \\ We propose and study a method to accelerate the verification of reachability problems in Petri nets based on structural reductions. This approach, that we call polyhedral reduction, relies on a state space abstraction that combines structural reductions and linear arithmetic constraints on the marking of places. The correctness of this method is based on a new notion of equivalence between nets. Combined with an SMT-based model checker, one can transform a reachability problem about some Petri net, into the verification of an equivalent reachability property on a reduced version of this net. We also propose an automated procedure to prove that such an abstraction is correct, exploiting a connection with a class of Petri nets with Presburger-definable reachability sets. In addition, we present a data structure, called Token Flow Graph (TFG), that captures the particular structure of constraints stemming from structural reductions. We leverage TFGs to efficiently solve two problems. First, to eliminate quantifiers that appear during our transformation, in the updated formula to be checked on the reduced net. Second, to compute the concurrency relation of a net, that is all pairs of places that can be marked simultaneously in some reachable marking. We apply our approach to several symbolic model checking procedures and introduce a new semi-decision procedure for checking reachability properties in Petri nets based on the Property Directed Reachability (PDR) method. A distinctive feature of this PDR method is its ability to generate verdict certificates that can be verified using an external SMT solver. Our approach and algorithms are implemented in four open-source tools: SMPT for checking reachability properties; Kong for accelerating the computation of concurrent places; Octant for eliminating quantifiers; and Reductron for automatically proving the correctness of polyhedral reductions. We give experimental results about their effectiveness, both for bounded and unbounded nets, using a large benchmark provided by the Model Checking Contest. [[en:seminaires:verif:index|Verification]]\\ Monday May 13, 2024, 11AM, 3052 and [[https://u-paris.zoom.us/j/89886269671?pwd=QlgvOVBmdjZTVGZqamdOWVdSWWU5UT09|Zoom link]]\\ **Enrique Román Calvo** (IRIF) //Dynamic Partial Order Reduction for Checking Correctness against Transaction Isolation Levels// \\ Modern applications, such as social networking systems and e-commerce platforms are centered around using large-scale databases for storing and retrieving data. Accesses to the database are typically enclosed in transactions that allow computations on shared data to be isolated from other concurrent computations and resilient to failures. Modern databases trade isolation for performance. The weaker the isolation level is, the more behaviors a database is allowed to exhibit and it is up to the developer to ensure that their application can tolerate those behaviors. In this work, we propose stateless model checking algorithms for studying correctness of such applications that rely on dynamic partial order reduction. These algorithms work for a number of widely-used weak isolation levels, including Read Committed, Causal Consistency, Snapshot Isolation and Serializability. We show that they are complete, sound and optimal, and run with polynomial memory consumption in all cases. We report on an implementation of these algorithms in the context of Java Pathfinder applied to a number of challenging applications drawn from the literature of distributed systems and databases. [[en:seminaires:verif:index|Verification]]\\ Monday May 6, 2024, 11AM, 3052 and [[https://u-paris.zoom.us/j/89886269671?pwd=QlgvOVBmdjZTVGZqamdOWVdSWWU5UT09|Zoom link]]\\ **Giovanni Bernardi** (IRIF) //Constructive characterisations of the must-preorder for asynchrony// \\ De Nicola and Hennessy’s must-preorder is a contextual refinement which states that a server q refines a server p if all clients satisfied by p are also satisfied by q. Owing to the universal quantification over clients, this definition does not yied a practical proof method for the must-preorder, and alternative characterisations are necessary to reason on it. I will outline the first characterisations of the must-preorder that are constructive, supported by a mechanisation in Coq, and independent from any calculus: the results pertain to Selinger output-buffered agents with feedback. This is a class of Labelled Transition Systems that captures programs that communicate asynchronously via a shared unordered buffer, as in asynchronous CCS or the asynchronous π-calculus. The results are surprising: the behavioural characterisations devised for synchronous communication carry over as they stand to the asynchronous setting, if servers are enhanced to act as forwarders, i.e. they can input any message as long as they store it back into the shared buffer. [[en:seminaires:verif:index|Verification]]\\ Monday April 29, 2024, 11AM, 3052 and [[https://u-paris.zoom.us/j/89886269671?pwd=QlgvOVBmdjZTVGZqamdOWVdSWWU5UT09|Zoom link]]\\ **Niklas Kochdumper** (IRIF) //Neural Network Verification using Polynomial Zonotopes// \\ Since artificial intelligence is nowadays also increasingly applied in safety-critical applications such as autonomous driving and human robot collaboration, there is an urgent need for approaches that can efficiently verify that the corresponding neural networks are safe. In general, verification tasks involving neural networks can be classified into the two groups open-loop verification and closed-loop verification. For open-loop verification one aims to prove certain properties of a standalone neural network, while for closed-loop verification the neural network acts as a controller for a dynamic system. This presentation demonstrates a novel verification technique that is based on a polynomial abstraction of the input-output-relation of the single neurons, which proves to be beneficial for both open- as well as closed-loop neural network verification. [[en:seminaires:verif:index|Verification]]\\ Monday April 22, 2024, 11AM, 3052 (streamed) and [[https://u-paris.zoom.us/j/89886269671?pwd=QlgvOVBmdjZTVGZqamdOWVdSWWU5UT09|Zoom link]]\\ **Sidi Mohamed Beillahi** (University of Toronto) //Securing Smart Contracts Through Program Synthesis// \\ In decentralized finance (DeFi), malicious adversaries were able to steal over 2 billions dollars in crypto assets over the past two years. One very common strategy malicious adversaries use is to borrow large assets through flash loans to launch their exploits against vulnerable DeFi smart contracts deployed on the Blockchain. Flash loans are loans that are only valid within a blockchain transaction and must be repaid with fees by the end of that transaction. Unlike normal loans, flash loans allow borrowers to borrow large assets without upfront collateral deposits. In this talk, I will first present a work on automated synthesis of adversarial transactions that exploit DeFi smart contracts using flash loans. To bypass the complexity of a DeFi protocol and needs for source code analysis, we propose a new technique to approximate the DeFi protocol functional behaviors using numerical methods (polynomial linear regression and nearest-neighbor interpolation). We then construct an optimization query using the approximated functions of the DeFi protocol to find an adversarial attack that is constituted of a sequence of functions invocations with optimal parameters that provides the maximum profit. To improve the accuracy of the approximation, we propose a novel counterexample driven approximation refinement technique. I will then present a followup work studying a category of DeFi attacks known as oracle manipulation attacks and the effectiveness of the current mechanisms used to protect against those attacks. I will show that those mechanisms are inadequate to ensure DeFi smart contracts safety when confronted with significant oracle deviations. I will then present a new framework to identify parameters that allow to secure DeFi smart contracts against oracle manipulation attacks. In the framework, we first perform symbolic analysis on the given contract and construct a summary model of constraints. We then leverage an SMT solver to identify parameters values that allow to secure smart contracts against oracle deviations. The talk is based on two ICSE 2024 papers that are joint works with Zhiyang Chen, Xun Deng, Andreas Veneris, and Fan Long (University of Toronto) and Cyrus Minwalla and Han Du (Bank of Canada). [[en:seminaires:verif:index|Verification]]\\ Monday March 25, 2024, 11AM, 3052 and [[https://u-paris.zoom.us/j/89886269671?pwd=QlgvOVBmdjZTVGZqamdOWVdSWWU5UT09|Zoom link]]\\ **Étienne André** (LIPN) //Monitoring cyber-physical systems under uncertainty// \\ Monitoring cyber-physical systems attracts both scientific and practical attention. However, monitoring algorithms suffer from the methodological difficulty of only observing sampled discrete-time signals gathered in a log, while real behaviors are continuous-time signals, which implies some uncertainty. In addition, the monitoring properties can themselves feature some uncertainty: e.g., a period in a property to be monitored can be uncertain or even unknown. In this presentation, we present two ways to address uncertainty while monitoring cyber-physical systems. First, we address timed pattern matching in the presence of an uncertain specification. We want to know for which start and end dates in a log, and for what values of the timing parameters, a property holds. For instance, we look for the minimum or maximum period (together with the corresponding start and end dates) for which the property holds. We rely on two solutions, one based on model-checking, and the other one being ad-hoc. Second, to mitigate the problem of sampling uncertainties, we introduce a model-bounded monitoring scheme, where we use a (limited) prior knowledge about the target system in order to prune interpolation candidates. We express such prior knowledge by linear hybrid automata (LHAs)---the LHAs are called bounding models. We rely on reachability techniques for linear hybrid automata using polyhedra to efficiently decide whether the property holds on a given log. We implemented both approaches, and experiments on realistic benchmarks show that both directions are efficient and practically relevant. This presentation is mainly based on publications at ACM ToSEM (2023) ACM ToCPS (2022), and are joint work with Masaki Waga (Kyoto University) and Ichiro Hasuo (NII, Tokyo, Japan). [[en:seminaires:verif:index|Verification]]\\ Monday March 18, 2024, 11AM, 3052 and [[https://u-paris.zoom.us/j/89886269671?pwd=QlgvOVBmdjZTVGZqamdOWVdSWWU5UT09|Zoom link]]\\ **Sarah Winter** (IRIF) //Deterministic Regular Functions of Infinite Words// \\ Regular functions of infinite words are (partial) functions realized by deterministic two-way transducers with infinite look-ahead. Equivalently, Alur et. al. have shown that they correspond to functions realized by deterministic Muller streaming string transducers, and to functions defined by MSO-transductions. Regular functions are however not computable in general (for a classical extension of Turing computability to infinite inputs), and we consider in this paper the class of deterministic regular functions of infinite words, realized by deterministic two-way transducers without look-ahead. We prove that it is a well-behaved class of functions: they are computable, closed under composition, characterized by the guarded fragment of MSO-transductions, by deterministic Büchi streaming string transducers, by deterministic two-way transducers with finite look-ahead, and by finite compositions of sequential functions and one fixed basic function called map-copy-reverse. This is joint work with Olivier Carton, Gaëtan Douéneau-Tabot, and Emmanuel Filiot. [[en:seminaires:verif:index|Verification]]\\ Monday March 11, 2024, 11AM, 3052 and [[https://u-paris.zoom.us/j/89886269671?pwd=QlgvOVBmdjZTVGZqamdOWVdSWWU5UT09|Zoom link]]\\ **Uli Fahrenberg** (LRE / EPITA) //Quantitative Verification: the Good, the Bad, the Ugly// \\ Quantitative verification is the verification of quantitative properties of quantitative systems. This is known to be difficult, notably because sweet spots are rare in-between robustness, compositionality and generalizability. In order to ensure robustness of verification, we replace the Boolean yes-no answers of standard verification with distances. Depending on the application context, many different types of distances are being employed in quantitative verification. Consequently, there is a need for a general theory of system distances which abstracts away from the concrete distances and develops quantitative verification at a level independent of the distance. We develop such a general theory, using games with quantitative objectives to define a quantitative version of van Glebbeek's linear-time-branching-time spectrum. We also extend this to a compositional theory of quantitative specifications, using disjunctive modal transition systems which capture precisely the greatest-fixed-point part of the mu-calculus, i.e. safety properties. We currently do not know how to go beyond safety properties. Another major obstacle is that we do not know how to integrate silent transitions into our framework. Finally, we argue that quantitative verification of real-time and hybrid systems poses other challenges which force us to look beyond our framework. The first 3/4 of this talk are based on the speaker's habilitation thesis which can be found at https://arxiv.org/abs/2204.11302 or https://hal.science/hal-04206693 [[en:seminaires:verif:index|Verification]]\\ Monday March 4, 2024, 11AM, 3052 and [[https://u-paris.zoom.us/j/89886269671?pwd=QlgvOVBmdjZTVGZqamdOWVdSWWU5UT09|Zoom link]]\\ **Adrian Francalanza** (University of Malta) //An Operational Guide to Monitorability// \\ Monitorability underpins the technique of Runtime Verification because it delineates what properties can be verified at runtime. Although many monitorability definitions exist, few are defined explicitly in terms of the operational guarantees provided by monitors, i.e., the computational entities carrying out the verification. This work views monitorability as a spectrum, where the fewer guarantees that are required of monitors, the more properties become monitorable. Accordingly, we present a monitorability hierarchy based on this trade-off. For regular specifications, we give syntactic characterisations in Hennessy–Milner logic with recursion for its levels. Finally, we map existing monitorability definitions into our hierarchy. This gives a unified framework that makes the operational assumptions and guarantees of each definition explicit and provides a rigorous foundation that can inform design choices and correctness claims for runtime verification tools. This is joint work with Luca Aceto, Antonis Achilleos, Anna Ingolfsdottir and Karoliina Lehtinen [[en:seminaires:verif:index|Verification]]\\ Monday February 26, 2024, 11AM, 3052 and [[https://u-paris.zoom.us/j/89886269671?pwd=QlgvOVBmdjZTVGZqamdOWVdSWWU5UT09|Zoom link]]\\ **Loïc Germerie Guizouarn** (Université Paris-Est Créteil) //Quasi-synchronous communications and verification of distributed systems// \\ Distributed systems are typically based on asynchronous exchanges of messages. Communicating automata are a tool to reason formally on the communications of such systems, allowing to detect automatically errors, like deadlocks or loss of messages. Detecting these errors is undecidable in general for systems with two or more participants, and several restrictions of the model have been considered to restore decidability. The subject of this presentation is one of these approaches, based on systems whose executions are realisable with synchronous communications (RSC). The behaviour of these systems approximate synchronous behaviours, where messages are sent and received in an atomic action. [[en:seminaires:verif:index|Verification]]\\ Monday February 19, 2024, 11AM, 3052 and [[https://u-paris.zoom.us/j/89886269671?pwd=QlgvOVBmdjZTVGZqamdOWVdSWWU5UT09|Zoom link]]\\ **Dylan Marinho** (Telecom SudParis) //Execution-time opacity problems in (parametric) timed automata// \\ Among harmful information leaks, the timing information leakage is the ability for an attacker to deduce internal information depending on timing information. In this presentation, I focus on timing leakage through the total execution time, i. e., when a system works as an almost black-box and the ability of the attacker is limited to know the model and observe the total execution time. I will present the formalization we introduced with timed automata and how we can verify security properties in timed systems. This presentation is mainly based on publications at ACM TOSEM (2022), FTSCS 2022 and ICECCS 2023, and on join works with Étienne André, Shapagat Bolat, Engel Lefaucheux, Didier Lime and Sun Jun. [[en:seminaires:verif:index|Verification]]\\ Monday February 12, 2024, 11AM, 3052 and [[https://u-paris.zoom.us/j/89886269671?pwd=QlgvOVBmdjZTVGZqamdOWVdSWWU5UT09|Zoom link]]\\ **Jawher Jerray** (Télécom Paris) //Guaranteed properties of real-time systems under perturbations.// \\ Since real-time systems has a major impact on human development, especially critical systems that can put human lives at risk if something goes wrong. Hence, the need of studying the behavior of these systems in order to guarantee their correct functioning. Nevertheless, computing such type of system has never been an easy task, as the complexity of these systems is constantly increasing, in addition to the perturbations that may arise during their performance, as well as undefined parameters that may exist. To ensure that a system always produces the expected results and does not fail in any way, a formal verification of its behavior and properties is necessary. In this work, we study the schedulability of the flight control of a space launcher with unknown parameters and under constraints. Then, we propose a synthesis of the admissible timing values of the unknown parameters by a parametric timed model checker. We increase the complexity of the problem by taking into consideration the switch time between two threads. We extend this work by developing a tool that translates a given real-time system design into parametric timed automata in order to infer some timing constraints ensuring schedulability. [[en:seminaires:verif:index|Verification]]\\ Monday February 5, 2024, 11AM, [[https://u-paris.zoom.us/j/89886269671?pwd=QlgvOVBmdjZTVGZqamdOWVdSWWU5UT09|Zoom link]]\\ **Tayssir Touili** (LIPN) //On static malware detection// \\ The number of malware is growing extraordinarily fast. A malware may bring serious damage. Thus, it is crucial to have efficient up-to-date virus detectors. Existing antivirus systems use various detection techniques to identify viruses such as (1) code emulation where the virus is executed in a virtual environment to get detected; or (2) signature detection, where a signature is a pattern of program code that characterizes the virus. A file is declared as a virus if it contains a sequence of binary code instructions that matches one of the known signatures. These techniques are becoming insufficient. Indeed, emulation based techniques can only check the program's behavior in a limited time interval. As for signature based systems, it is very easy to virus developers to get around them. Thus, a robust malware detection technique needs to check the behavior (not the syntax) of the program without executing it. We show in this talk how using behavior signatures allow to efficiently detect malwares in a completely static way. We implemented our techniques in a tool, and we applied it to detect several viruses. Our results are encouraging. In particular, our tool was able to detect more than 800 viruses. Several of these viruses could not be detected by well-known anti-viruses such as Avira, Avast, Norton, Kaspersky and McAfee. [[en:seminaires:verif:index|Verification]]\\ Monday January 15, 2024, 11AM, 3052 and [[https://u-paris.zoom.us/j/89886269671?pwd=QlgvOVBmdjZTVGZqamdOWVdSWWU5UT09|Zoom link]]\\ **Raphaël Berthon** (Aachen University) //Natural Strategic Ability in Stochastic Multi-Agent Systems// \\ Synthesis under partial information often leads to undecidability or very high complexity, but bounding the available memory has recently proved to be an effective solution. On Multi-Agent Systems (MAS), it is also necessary to balance between the ability of agents to strategize with memory and the model-checking complexity, but until now it has been restricted to fully deterministic settings. We propose the use of natural strategies to reason about the probabilistic temporal logics PATL and PATL* under some partial information. As a main result we show that, in stochastic MAS, NatPATL model-checking is NP-complete when the active coalition is restricted to deterministic strategies. [[en:seminaires:verif:index|Verification]]\\ Monday January 8, 2024, 11AM, 3052 and [[https://u-paris.zoom.us/j/89886269671?pwd=QlgvOVBmdjZTVGZqamdOWVdSWWU5UT09|Zoom link]]\\ **Henry Sinclair-Banks** (University of Warwick) //Coverability in VASS Revisited: Improving Rackoff’s Bound to Obtain Conditional Optimality// \\ Vector Addition Systems with States (VASS) are a long-studied model that are equivalent to Petri nets. The coverability problem asks whether there exists a run from a given initial configuration to a configuration that is at least a given target configuration. Coverability is in EXPSPACE (Rackoff '78) and is EXPSPACE-hard already under unary encodings (Lipton '76). Rackoff's upper bound is derived by considering the necessary length of runs that witness coverability. In this presentation, I will present an improved upper bound on the lengths of such runs. The run length bound can be used to obtain two algorithms: an optimal exponential space algorithm and a conditionally optimal double-exponential time algorithm. I aim to show the double-exponential time lower bound that is conditioned upon the Exponential Time Hypothesis (ETH). About joint work with Marvin Künnemann, Filip Mazowiecki, Lia Schütze, and Karol Węgrzycki (ICALP’23).