Aarhus University Seal

Program


Monday 25 August 2025

08:30-09:00

Registration and coffee


09:00-09:50

SynCoP 2025

Room: M2.3
Program

RADICAL 2025

Room: M1
Program

FMQC 2025

Room: M2
Program

BMQL 2025

Room: M2.2
Program


09:50-10:20

Coffee break


10:20-12:00

SynCoP 2025

Room: M2.3
Program

RADICAL 2025

Room: M1
Program

FMQC 2025

Room: M2
Program

BMQL 2025

Room: M2.2
Program


12:00-13:30

Lunch

Vandrehallen


13:30-14:20

SynCoP 2025

Room: M2.3
Program

RADICAL 2025

Room: M1
Program

FMQC 2025

Room: M2
Program

BMQL 2025

Room: M2.2
Program

Express/SOS 2025

Room: Richard Mortensen
Program


14:20-14:40

Coffee break


14:40-15:55

SynCoP 2025

Room: M2.3
Program

RADICAL 2025

Room: M1
Program

FMQC 2025

Room: M2
Program

BMQL 2025

Room: M2.2
Program

Express/SOS 2025

Room: Richard Mortensen
Program


15:55-16:15

Coffee break


16:15-17:30

SynCoP 2025

Room: M2.3
Program

RADICAL 2025

Room: M1
Program

FMQC 2025

Room: M2
Program

BMQL 2025

Room: M2.2
Program

Express/SOS 2025

Room: Richard Mortensen
Program

Tuesday 26 August 2025


08:30-08:50

Registration and coffee


08:50-09:00

Opening Jaco van de Pol

Stakladen


09:00-09:50

INVITED SPEAKER QEST+FORMATS

Stakladen
Session chair: TBA

Christoph Matheja

Automating Proof Rules for Probabilistic Programs


09:50-10:20

Coffee break


10:20-12:00

CONCUR

Stakladen

TEMPORAL LOGICS - I

Chair: Orna Grumberg

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

QEST+FORMATS

M2

STATISTICAL MODEL CHECKING AND APPROXIMATIONS

PyDSMC: Statistical Model Checking for Neural Agents Using the Gymnasium Interface

Timo P. Gros, Arnd Hartmanns, Ivo Hoese, Joshua Meyer, Nicola J. Müller and Verena Wolf    

What Are the Odds? Improving Statistical Model Checking of Markov Decision Processes

Patrick Wienhöft, Tobias Meggendorfer and Maximilian Weininger

Time-Sensitive Importance Splitting

Gabriel Dengler, Carlos E. Budde, Laura Carnevali and Arnd Hartmanns

Conservation Analysis and Discrete Probabilistic Approximations for Parameter Estimation of Biochemical Networks

Olivier Bouët-Willaumez, Adrien Le Coënt, Benoit Barbot and Nihal Pekergin


12:00-13:30

Lunch

Vandrehallen


13:30-14:20

CONCUR

Stakladen

INVITED SPEAKER CONCUR

Chair: Wan Fokkink

Jiri Srba

On-the-Fly Verification: Advancements in Dependency Graphs

QEST+FORMATS

M2

TIMED AUTOMATA

Using Communication to Bound Clock Drift in Local-Timed Negotiations

Abhinav Garg, Madhavan Mukund, Adwitee Roy, B Srivathsan and Gautham Viswanathan

Signal Sampling and Optimisation under Symbolic Timed Automata Constraints

Benoit Barbot, Nicolas Basset, Thao Dang, Alexandre Donzé, Marco Esposito and Dejan Nickovic


14:20-14:40

Coffee break


14:40-15:55

CONCUR

Stakladen

GAMES - I

Chair: Marielle Stoelinga

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

QEST+FORMATS

M2

DYNAMICAL SYSTEMS

Computing the Congestion Phases of Dynamical Systems with Priorities and Application to Emergency Departments

Xavier Allamigeon, Pascal Capetillo and Stéphane Gaubert

Modeling Uncertainty: From Simulink to Stochastic Hybrid Automata

Pauline Blohm, Felix Schulz, Lisa Willemsen, Anne Remke and Paula Herber

Symbolic Reduction for Formal Synthesis of Global Lyapunov Functions

Jun Liu and Maxwell Fitzsimmons


15:55-16:15

Coffee break


16:15-17:30

CONCUR

Stakladen

PROBABILISTIC SYSTEMS

Chair: Christel Baier

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

QEST+FORMATS

M2

QUEUEING THEORY

Minimal Per-Flow Backlog Bounds at an Aggregate FIFO Server under Piecewise-Linear Arrival Curves

Lukas Wildberger, Anja Hamscher and Jens B. Schmitt

Formal Approximations of the Transient Distributions of the M/G/1 Workload Process

Fabian Michel and Markus Siegle

A Product-Form Model for Systems with Aging Objects and Similarities

Andrea Marin, Diletta Olliaro, Sabina Rossi and Daniel Sadoc Menasche


18.30-21.00

Welcome Reception

Salling Rooftop

Wednesday 27 August 2025

08:30-09:00

Registration and coffee


09:00-9:50

INVITED SPEAKER FMICS

Stakladen

Ina Schieferdecker

Navigating the growing field of research on AI for software testing – taxonomy and survey


09:50-10:20

Coffee break


10:20-12:00

CONCUR

Stakladen

PROCESS ALGEBRA, EQUIVALENCES - I

Chair: Rob van Glabbeek

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

QEST+FORMATS

M2

GAMES AND CONTROL

A Hyperlogic for Strategies in Stochastic Games

Lina Gerlach, Christof Löding and Erika Abraham

Controller Synthesis for Parametric Timed Games

Mikael Bisgaard Dahlsen-Jensen, Baptiste Fievet, Jaco van de Pol and Laure Petrucci

Formal Control for Uncertain Systems via Contract-Based Probabilistic Surrogates

Oliver Schön, Sofie Haesaert and Sadegh Soudjani

On Choice of Loss Functions for Neural Control Barrier Certificates

Alireza Nadali, Ashutosh Trivedi and Majid Zamani

FMICS

M1

VERIFICATION

End-to-End Formal Methods Integrated Development with SysMLv2 using HAMR

Stefan Hallerstede, Robby, John Hatcliff, Jason Belt and David Hardin

AutoSV-Annotator: Integrating Deductive and Automatic Software Verification 

Lukas Armborst, Dirk Beyer, Marieke Huisman and Marian Lingsch-Rosenfeld

IC3 for Loop Invariant Generation in Deductive Verification of Control Code

Niklas van de Sand and Marcus Völker

Backward Responsibility in Transition Systems Beyond Safety

Christel Baier, Rio Klatt, Sascha Klüppelholz and Johannes Lehmann


12:00-13:30

Lunch

Vandrehallen


13:30-14:20

INVITED SPEAKER QEST+FORMATS

Stakladen
Chair: TBA

Alessandro Abate

Neural synthesis for verification and control of stochastic systems - certificates and abstractions


14:20-14:40

Coffee break


14:40-15:55

CONCUR

Stakladen

CONCURRENT SYSTEMS

Chair: Joost-Pieter Katoen

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

QEST+FORMATS

M2

PROBABILISTIC SYSTEMS ANALYSIS

Programming and Reasoning in Partially Observable Probabilistic Environments

Tobias Gürtler and Benjamin Lucien Kaminski

Statistical Model Checking Beyond Means: Quantiles, CVaR, and the DKW Inequality

Carlos E. Budde, Arnd Hartmanns, Tobias Meggendorfer, Maximilian Weininger and Patrick Wienhöft

Numerical Errors in Quantitative System Analysis With Decision Diagrams

Sebastiaan Brand, Arend-Jan Quist, Richard M.K. van Dijk and Alfons Laarman

FMICS

M1

AUTOMOTIVE AND RAILWAY

GRust: A Programming Language for Automotive Engineering

Émilie Thomé, Christine Tasson and Xavier Denis

Robust Spatio-Temporal Logic Semantics for Autonomous Driving Systems Falsification

Tiago Sequeira and André Pedro

Data-Driven Synthesis of Stochastic Fault Trees for Proactive Maintenance of Railway Vehicles

Laura Carnevali, Alessandro Fantechi, Gloria Gori, Denis Vreshtazi, Alessandro Borselli, Maria Rosaria Cefaloni and Lucio Rota


15:55-16:15

Coffee break


16:15-17:30

CONCUR

Stakladen

GAMES - II

Chair: Martin Zimmermann

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

QEST+FORMATS

M2

LEARNING AND INFERENCE

Active Learning of Mealy Machines with Timers

Véronique Bruyère, Bharat Garhewal, Guillermo Perez, Gaëtan Staquet and Frits Vaandrager    

Learning Mealy Machines with Sparse Observation Tables

Wolffhardt Schwabe, Paul Kogel and Sabine Glesner    

Statistical Bayesian Inference for Stochastic Process Discovery

Paolo Ballarini, Pierre Cry, Andras Horvath and Pascale Legall    

FMICS

M1

CYBER-PHYSICAL SYSTEMS

Promise-Driven Modeling: A Structured Approach for Modeling Cyber- Physical Systems

Felix Schaber, Atif Mashkoor and Michael Leuschel

Ensuring Integration Conditions during the Update of Cyber-Physical Systems at Runtime

Janis Kröger, Ingo Stierand and Martin Fränzle

Thursday 28 August 2025

08:30-09:00


Registration and coffee


09:00-9:50

CONCUR

Stakladen

INVITED SPEAKER

Chair: Patricia Bouyer

Christel Baier

Linear Temporal Logic with Standpoint Modalities

QEST+FORMATS

M2

SECURITY

Fuzzy Fault Trees: the Fast and the Formal

Thi Kim Nhung Dang, Benedikt Peterseim, Milan Lopuhaä-Zwakenberg and Mariëlle Stoelinga    

Noninterference Analysis of Deterministically Timed Reversible Systems

Andrea Esposito, Alessandro Aldini and Marco Bernardo    

FMICS

M1

PROGRAM VERIFICATION

A Complete Formal Specification and Verification of the BESW software control system of the Maeslant Storm Surge Barrier

Adrian Beers, Jore Booy, Jan Friso Groote, Johan van den Bogaard and Mark Bouwman

Proof Engineering in Logika: Synergistically Integrating Automated and Semi-Automated Program Verification

Stefan HallerstedeRobby, John Hatcliff, Jason Belt and David Hardin


09:50-10:10

Coffee break


10:10-11:00

CONCUR

Stakladen

TEMPORAL LOGICS - II

Chair: Frits Vaandrager

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

QEST+FORMATS

M2

INVITED SPEAKER

Lu Feng

Runtime Safety for Learning-Enabled Cyber-Physical Systems: From Predictive Monitoring to Adaptive Shielding

FMICS

M1

EMBEDDED SYSTEMS

A Specification-Driven Approach to Embedded FDIR Code Generation

Federico Bonafini, Roberto Cavada, Alessandro Cimatti, Guillermo, Gomez and Stefano Tonetta

Building a Modular Platform for Model Checking Glitch Attacks in RISC-V Programs

Andreas Brandhøj, Tobias Worm Bøgedal, René Rydhof Hansen,Kim Larsen and Danny Poulsen


11:00-11:20

Coffee break


11:20-12:10

CONCUR

Stakladen

PROCESS ALGEBRA, EQUIVALENCES - II

Chair: Jan Friso Groote

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

QEST+FORMATS

M2

TERMINATION AND DECIDABILITY

Tightening the Frontier of Decidability for Decisiveness

Gaspard Fougea, Serge Haddad, Lina Ye, Shreyas Jain and Alain Finkel    

*Positive Almost-Sure Termination of Polynomial Random Walks

Lorenz Winkler and Laura Kovács    

FMICS

M1

INVITED SPEAKER

Arnd Hartmanns

An Overview of Sound and Modest Approaches to Quantitative Model Checking from Sea to Space


12:10-13:30

Lunch

Vandrehallen


13:30-14:30

Steering Committee Meetings


15:30-21:00

Social event + Dinner

Art museum ARoS

Friday 29 August 2025

08:30-09:00

Registration and coffee


09:00-9:50

INVITED SPEAKER CONCUR

Stakladen
Chair: Jaco van de Pol

Chris Heunen

Towards categorical quantum concurrency theory


09:50-10:20

Coffee break


10:20-12:00

CONCUR

Stakladen

AUTOMATA, TRANSDUCERS, LEARNING

Chair: Kim Larsen

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


12:00-13:30

Lunch

Vandrehallen


13:30-14:20

CONCUR

Stakladen

VECTOR ADDITION SYSTEMS

Chair: Jiri Srba

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:20-14:40

Coffee break


14:40-15:55

CONCUR

Stakladen

MONITORABILITY, QUANTITATIVE AUTOMATA

Chair: Pedro D'Argenio

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


15:55-16:15

Coffee break


16:15-17:30

CONCUR

Stakladen

TYPES, SEMANTICS

Chair: Patricia Bouyer

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