Table of Contents

• Front Matter, Table of Contents, Preface, Conference Organization [doi]
• (Metric) Bisimulation Games and Real-Valued Modal Logics for CoalgebrasBarbara König 0001, Christina Mika-Michalski. [doi]
• Verifying Quantitative Temporal Properties of Procedural ProgramsMohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, Prakash Saivasan. [doi]
• Automated Detection of Serializability Violations Under Weak ConsistencyKartik Nagar, Suresh Jagannathan. [doi]
• The Satisfiability Problem for Unbounded Fragments of Probabilistic CTLJan Kretínský, Alexej Rotar. [doi]
• Effective Divergence Analysis for Linear Recurrence SequencesShaull Almagor, Brynmor Chapman, Mehran Hosseini, Joël Ouaknine, James Worrell 0001. [doi]
• Deciding Probabilistic Bisimilarity Distance One for Probabilistic AutomataQiyi Tang, Franck van Breugel. [doi]
• Synchronizing the AsynchronousBernhard Kragl, Shaz Qadeer, Thomas A. Henzinger. [doi]
• Progress-Preserving Refinements of CTAMassimo Bartoletti, Laura Bocchi, Maurizio Murgia. [doi]
• Verifying Arithmetic Assembly Programs in Cryptographic Primitives (Invited Talk)Andy Polyakov, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang. [doi]
• Universal Safety for Timed Petri Nets is PSPACE-completeParosh Aziz Abdulla, Mohamed Faouzi Atig, Radu Ciobanu, Richard Mayr, Patrick Totzke. [doi]
• Non-deterministic Weighted Automata on Random WordsJakub Michaliszyn, Jan Otop. [doi]
• Affine Extensions of Integer Vector Addition Systems with StatesMichael Blondin, Christoph Haase, Filip Mazowiecki. [doi]
• A Coalgebraic Take on Regular and omega-Regular Behaviour for Systems with Internal MovesTomasz Brengos. [doi]
• Automatic Analysis of Expected Termination Time for Population ProtocolsMichael Blondin, Javier Esparza, Antonín Kucera. [doi]
• On Runtime Enforcement via SuppressionsLuca Aceto, Ian Cassar, Adrian Francalanza, Anna Ingólfsdóttir. [doi]
• It Is Easy to Be Wise After the Event: Communicating Finite-State Machines Capture First-Order Logic with "Happened Before"Benedikt Bollig, Marie Fortin, Paul Gastin. [doi]
• The Complexity of Rational Synthesis for Concurrent GamesRodica Condurache, Youssouf Oualhadj, Nicolas Troquard. [doi]
• Relating Syntactic and Semantic Perturbations of Hybrid AutomataNima Roohi, Pavithra Prabhakar, Mahesh Viswanathan 0001. [doi]
• Alternating Nonzero AutomataPaulin Fournier, Hugo Gimbert. [doi]
• A Semantics for Hybrid IterationSergey Goncharov 0001, Julian Jakob, Renato Neves. [doi]
• Selective MonitoringRadu Grigore, Stefan Kiefer. [doi]
• Reachability in Timed Automata with Diagonal ConstraintsPaul Gastin, Sayan Mukherjee, B. Srivathsan. [doi]
• Ergodic Mean-Payoff Games for the Analysis of Attacks in Crypto-CurrenciesKrishnendu Chatterjee, Amir Kafshdar Goharshady, Rasmus Ibsen-Jensen, Yaron Velner. [doi]
• Reachability in Parameterized Systems: All Flavors of Threshold AutomataJure Kukovec, Igor Konnov 0001, Josef Widder. [doi]
• GPU Schedulers: How Fair Is Fair Enough?Tyler Sorensen, Hugues Evrard, Alastair F. Donaldson. [doi]
• Learning-Based Mean-Payoff Optimization in an Unknown MDP under Omega-Regular ConstraintsJan Kretínský, Guillermo A. Pérez, Jean-François Raskin. [doi]
• Regular Separability of Well-Structured Transition SystemsWojciech Czerwinski, Slawomir Lasota, Roland Meyer, Sebastian Muskalla, K. Narayan Kumar, Prakash Saivasan. [doi]
• Logics Meet 1-Clock Alternating Timed AutomataShankara Narayanan Krishna, Khushraj Madnani, Paritosh K. Pandya. [doi]
• Is Speed-Independent Mutual Exclusion Implementable? (Invited Talk)Rob van Glabbeek. [doi]
• Narrowing down the Hardness Barrier of Synthesizing Elementary Net SystemsRonny Tredup, Christian Rosenke. [doi]
• Verification of Immediate Observation Population ProtocolsJavier Esparza, Pierre Ganty, Rupak Majumdar, Chana Weil-Kennedy. [doi]
• Up-To Techniques for Behavioural Metrics via FibrationsFilippo Bonchi, Barbara König 0001, Daniela Petrisan. [doi]
• Completeness for Identity-free Kleene LatticesAmina Doumane, Damien Pous. [doi]
• Parameterized complexity of games with monotonically ordered omega-regular objectivesVéronique Bruyère, Quentin Hautem, Jean-François Raskin. [doi]
• Separable GPL: Decidable Model Checking with More Non-DeterminismAndrey Gorlin, C. R. Ramakrishnan. [doi]
• Updating Probabilistic Knowledge on Condition/Event Nets using Bayesian NetworksBenjamin Cabrera, Tobias Heindel, Reiko Heckel, Barbara König 0001. [doi]
• A Universal Session Type for Untyped Asynchronous CommunicationStephanie Balzer, Frank Pfenning, Bernardo Toninho. [doi]
• Bisimulations for Probabilistic and Quantum Processes (Invited Paper)Yuxin Deng. [doi]
• Coalgebraic Theory of Büchi and Parity Automata: Fixed-Point Specifications, Categorically (Invited Tutorial)Ichiro Hasuo. [doi]
• The Siren Song of Temporal Synthesis (Invited Talk)Moshe Y. Vardi. [doi]
• Linear Equations with Ordered DataPiotr Hofman, Slawomir Lasota. [doi]
• Bounded Context Switching for Valence SystemsRoland Meyer, Sebastian Muskalla, Georg Zetzsche. [doi]