Aarhus University Seal

CONCUR 2025 - Program


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 Bisping Galois


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

New Fault Domains for Conformance Testing of Finite State Machines

Frits Vaandrager and Ivo Melse

Reversible Pebble Transducers

Luc Dartois, Paul Gastin, Loïc 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

VECTOR ADDITION SYSTEMS

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

MONITORABILITY, QUANTITATIVE AUTOMATA

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

Quantitative Language Automata

Thomas Henzinger, Pavol Kebis, Nicolas Mazzocchi and N. Ege Saraç

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