Tuesday 26 August 2025 | ||
| 9:00-9:50 | Invited speaker QEST+FORMATS | |
| Christoph Matheja Automating Proof Rules for Probabilistic Programs | ||
| 10:20-12:00 | TEMPORAL LOGICS - I | |
| Arbitrary-arity Tree Automata for QCTL Francois Laroussinie and Nicolas Markey | ||
| Prophecies all the Way: Game-based Model-Checking for HyperQPTL beyond ∀*∃* Sarah Winter and Martin Zimmermann | ||
| Characterizations of fragments of temporal logic over Mazurkiewikz traces Bharat Adsul, Paul Gastin and Shantanu Kulkarni | ||
| Model Checking as Program Verification by Abstract Interpretation Paolo Baldan, Roberto Bruni, Francesco Ranzato and Diletta Rigo | ||
| 13:30-14:20 | Invited speaker CONCUR | |
| Jiri Srba On-the-Fly Verification: Advancements in Dependency Graphs | ||
| 14:40-15:55 | GAMES - I | |
| Energy Games: To Solve All Kinds of Quantitative Reachability Problems Caroline Lemke and Benjamin BispingGalois | ||
| The Non-Cooperative Rational Synthesis Problem for Subgame Perfect Equilibria and omega-regular Objectives Véronique Bruyère, Jean-Francois Raskin, Alexis Reynouard and Marie Van Den Bogaard | ||
| Temporal Explorability Games Pete Austin, Sougata Bose, Nicolas Mazzocchi and Patrick Totzke | ||
| 16:15-17:30 | PROBABILISTIC SYSTEMS | |
| Chance and Mass Interpretations of Probabilities in Markov Decision Processes Yun Chen Tsai, Kittiphon Phalakarn, S. Akshay and Ichiro Hasuo | ||
| Omega-regular Verification and Control for Distributional Specifications in MDPs S. Akshay, Ouldouz Neysari and Đorđe Žikelić | ||
| Compositional Reasoning for Parametric Probabilistic Automata Hannah Mertens, Tim Quatmann and Joost-Pieter Katoen | ||
Wednesday 27 August 2025 | ||
| 9:00-9:50 | Invited speaker FMICS | |
| Ina Schieferdecker Navigating the growing field of research on AI for software testing – taxonomy and survey | ||
| 10:20-12:00 | PROCESS ALGEBRA, EQUIVALENCES - I | |
| From Bisimulation to Traces: The Impact of Parallel Composition on Finite Bases Rowin Versteeg, Valentina Castiglioni and Bas Luttik | ||
| A state-based O(m log n) partitioning algorithm for branching bisimilarity Jan Friso Groote and David N. Jansen | ||
| Explainability is a Game for Probabilistic Bisimilarity Distances Emily Vlasman, James Worrell, Anto Nanah Ji and Franck van Breugel | ||
| Open Bisimilarity for the π-calculus with Mismatch Tiange Liu, Alwen Tiu and Ross Horne | ||
| 13:30-14:20 | Invited speaker QEST+FORMATS: | |
| Alessandro Abate Neural synthesis for verification and control of stochastic systems - certificates and abstractions | ||
| 14:40-15:55 | CONCURRENT SYSTEMS | |
| Partial-Order Reduction Is Hard Frédéric Herbreteau, Sarah Larroze and Igor Walukiewicz | ||
| Optimal Concolic Dynamic Partial Order Reduction Mohammad Hossein Khoshechin Jorshari, Michalis Kokologiannakis, Rupak Majumdar and Srinidhi Nagendra | ||
| On the send-synchronizability problem for mailbox communication Romain Delpy, Anca Muscholl and Grégoire Sutre | ||
| 16:15-17:30 | GAMES - II | |
| Coverage Games Noam Shenwald and Orna Kupferman | ||
| A Direct Reduction from Parity to Simple Stochastic Games Raphaël Berthon, Joost-Pieter Katoen and Zihan Zhou | ||
| Expectation in Stochastic Games with Prefix-independent Objectives Laurent Doyen, Pranshu Gaba and Shibashis Guha | ||
Thursday 28 August 2025 | ||
| 9:00-9:50 | Invited speaker CONCUR | |
| Christel Baier Linear Temporal Logic with Standpoint Modalities | ||
| 10:10-11:00 | TEMPORAL LOGICS - II | |
| On-The-Fly Symbolic Algorithm for Timed ATL1 with Abstractions Nicolaj Østerby Jensen, Kim Guldstrand Larsen, Didier Lime and Jiri Srba | ||
| Expressive Equivalence Between Decidable Freeze and Metric Timed Temporal Logics Hsi-Ming Ho, S Krishna, Khushraj Madnani, Rupak Majumdar and Paritosh Pandya | ||
| 11:20-12:10 | PROCESS ALGEBRA, EQUIVALENCES - II | |
| First-order store and visibility in name-passing calculi Daniel Hirschkoff, Iwan Quémerais and Davide Sangiorgi | ||
| Just Verification of Mutual Exclusion Algorithms Rob van Glabbeek, Bas Luttik and Myrthe Spronck | ||
Friday 29 August 2025 | ||
| 9:00-9:50 | Invited speaker CONCUR | |
| Chris Heunen Towards categorical quantum concurrency theory | ||
| 10:20-12:00 | AUTOMATA, TRANSDUCERS, LEARNING | |
| Compositional Active Learning of Synchronous Systems through Automated Alphabet Refinement Leo Henry, Thomas Neele, Mohammad Mousavi and Matteo Sammartino | ||
| Quantitative Language Automata Thomas Henzinger, Pavol Kebis, Nicolas Mazzocchi and N. Ege Saraç | ||
| Reversible Pebble Transducers Luc Dartois, Paul Gastin, Loic Germerie Guizouarn and S Krishna | ||
| Resolving Nondeterminism by Chance Soumyajit Paul, David Purser, Sven Schewe, Qiyi Tang, Patrick Totzke and Di-De Yen | ||
| 13:30-14:20 | VASS | |
| Reachability in Vector Addition System with States Parameterized by Geometric Dimension Yangluo Zheng | ||
| Languages of Boundedly-Ambiguous Vector Addition Systems with States Wojciech Czerwiński and Łukasz Orlikowski | ||
| 14:40-15:55 | MONITORING | |
| Monitorability for the Modal µ-Calculus over Systems with Data: From Practice to Theory Luca Aceto, Antonis Achilleos, Ducan Paul Attard, Léo Exibard, Adrian Francalanza, Anna Ingolfsdottir and Karoliina Lehtinen | ||
| New Fault Domains for Conformance Testing of Finite State Machines Frits Vaandrager and Ivo Melse | ||
| Time for Timed Monitorability Thomas Møller Grosen, Sean Kauffman, Kim G. Larsen and Martin Zimmermann | ||
| 16:15-17:30 | TYPES, SEMANTICS | |
| Denotational Semantics for Probabilistic and Concurrent Programs Noam Zilberstein, Daniele Gorla and Alexandra Silva | ||
| A Sound and Complete Characterization of Fair Asynchronous Session Subtyping Mario Bravetti, Luca Padovani and Gianluigi Zavattaro | ||
| Abstract Subtyping for Asynchronous Multiparty Sessions Laura Bocchi, Andy King, Maurizio Murgia and Simon Thompson | ||
