Automating Proof Rules for Probabilistic Programs

Francois Laroussinie and Nicolas Markey

Sarah Winter and Martin Zimmermann

Bharat Adsul, Paul Gastin and Shantanu Kulkarni

Model Checking as Program Verification by Abstract Interpretation

Paolo Baldan, Roberto Bruni, Francesco Ranzato and Diletta Rigo

On-the-Fly Verification: Advancements in Dependency Graphs

Galois Energy Games: To Solve All Kinds of Quantitative Reachability Problems

Caroline Lemke and Benjamin Bisping

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

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

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

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

Alessandro Abate

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

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

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

Christel Baier

Linear Temporal Logic with Standpoint Modalities

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

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

Chris Heunen

Towards categorical quantum concurrency theory

Compositional Active Learning of Synchronizing Systems through Automated Alphabet Refinement

Léo Henry, Mohammad Reza Mousavi, Thomas Neele 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

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

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

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