Talks

Joint

• Reasoning About Probabilistic Loops, Moment by Moment

  Ezio Bartocci

  LiveInvited CONCUR FMICS Q+F 

• Category Theory for Fast Model Checking Algorithms

  Ichiro Hasuo

  LiveInvited CONCUR FMICS Q+F 

Invited

• On the role of prose in specifications

  Jade Alglave

  LiveCONCUR 

• An Introduction to Multi-Environment Markov Decision Processes

  Jean-François Raskin

  LiveCONCUR 

• Word Automata with Limited Nondeterminism

  Qiyi Tang

  LiveCONCUR 

• Reducing Time to Market through Formal Methods

  Colin O'Halloran

  LiveFMICS 

• Application of Formal Methods to Design and Verification of Autonomous Space Systems

  Julia Badger

  LiveFMICS 

• Reasoning About Probabilistic Loops, Moment by Moment

  Ezio Bartocci

  LiveJoint CONCUR FMICS Q+F 

• Category Theory for Fast Model Checking Algorithms

  Ichiro Hasuo

  LiveJoint CONCUR FMICS Q+F 

• QEST+FORMATS Opening

  on  Wed, 9:00 Live in  Room B

  Q+F 

• Supporting Older Adults Living Independently

  Jane Hillston

  LiveQ+F 

• Monitoring of Timed and Quantitative Systems

  Kim G. Larsen

  LiveQ+F 

CONCUR

• On the role of prose in specifications

  Jade Alglave

  LiveInvited 

• An Introduction to Multi-Environment Markov Decision Processes

  Jean-François Raskin

  LiveInvited 

• Word Automata with Limited Nondeterminism

  Qiyi Tang

  LiveInvited 

• Algebraic Characterization of FO-definable Languages of Higher-Dimensional Automata

  Enzo Erlich, Jérémy Ledent, Krzysztof Ziemiański

• Asymmetrically-Discounted Stochastic Games

  Sarvin Bahmani, Soumyajit Paul, Sven Schewe, Shadi Tasdighi Kalat, Ashutosh Trivedi

• PAC Learning in Turn-Based Stochastic Games with Reachability Objectives: A Decentralized Private Approach via Expected Conditional Distance

  Ali Asadi, Krishnendu Chatterjee, Pavol Kebis

• Prophecy-Based Automated Verification of Message-Passing Programs

  Takashi Nagatomi, Musashi Katsura, Naoki Kobayashi, Yusuke Matsushita, Ken Sakayori

• Wheeler Bisimulations

  Nicola Cotumaccio

• GKAT with Hoare Hypotheses

  Jurriaan Rot, Todd Schmid, Jana Wagemaker

• Decomposition of Automata recognizing Ideals

  Mathias Berry, Ismaël Jecker, Pierre-Cyrille Héam

• Compositionality in Coalgebraic Trace Semantics

  Robin Jourde, Henning Urbat, Sergey Goncharov, Stelios Tsampas, Jonas Forster

• Positional Properties in Temporal Logic

  Jessica Newman, Benjamin Plummer

• Threshold-Based Behavioural Distances

  Jonas Forster, Lutz Schröder, Paul Wild, Barbara König, Pedro Nora

• An MSO Framework for Weak-Memory Verification and Robustness

  Giovanna Kobus Conrado, Andreas Pavlogiannis

• Graded Semantics of Nominal Systems

  Hannes Schulze, Lutz Schröder, Üsame Cengiz

• Concurrent Visibility: higher-order concurrency with first-order store

  Iwan Quémerais, Guilhème Jaber, Ken Sakayori, Davide Sangiorgi

• Improving Reachability in Vector Addition Systems through Pumpability

  Weijun Chen, Yuxi Fu, Yangluo Zheng

• Reaching as Cheap as Possible in 1-clock Robust Weighted Timed Games

  Nathalie Bertrand, Maëlle Gautrin, Julie Parreaux

• Completeness for Probabilistic Boolean Tapes

  Filippo Bonchi, Cipriano Junior Cioffo

• Revisiting True Concurrency Bisimilarities: On the Role of Backward Ready Multisets and Why They Are Not Enough for HPB and HHPB

  Andrea Esposito, Marco Bernardo

• On parameterized verification over tree topologies

  Romain Delpy, Anca Muscholl, Grégoire Sutre

• Coinductive reasoning for parametrized functors and monads

  Ugo Dal Lago, Zeinab Galal

• Classification under uncertainty

  Ofer Leshkowitz, Orna Kupferman

• Probabilistic Model Checking via Families of Deterministic and Unambiguous Finite Automata

  Christel Baier, Sascha Klüppelholz, Timm Spork

• WinPop: Making populations win together

  Nathalie Bertrand, Patricia Bouyer, Luc Lapointe, Corto Mascle

• Parameterized Verification of Asynchronous Round-Based Distributed Algorithms via Reduction to Finite-Counter Systems

  Nathalie Bertrand, Pranav Ghorpade, Sasha Rubin

• when Behaviours Have to Happen: An Axiomatic Model of Causality in Behaviour-Oriented Concurrency

  Luke Cheeseman, Elias Castegren, Tobias Wrigstad, Sophia Drossopoulou, Matthew Parkinson

• Complementing Emerson-Lei Elevator Automata

  Ondrej Alexaj, Vojtěch Havlena, Ondřej Lengál, Yong Li, Nicolas Mazzocchi

• Continuous Algebras with Hypotheses

  Lukas Mulder, Damien Pous, Jana Wagemaker

• A Factorization Theorem for Forest Algebras

  Shaull Almagor, Michaël Cadilhac, Asaf Shoham

• From Coalgebraic Determinization to Belief Construction for Partial Observability

  Mayuko Kori, Kazuki Watanabe

• Monitoring Discounted Sum Properties

  Filip Cano, Thomas A. Henzinger, Konstantin Kueffner, Ege Saraç

• Monadic Presburger Predicates have Robust Population Protocols

  Philipp Czerner, Javier Esparza, Vincent Fischer, Roland Guttenberg, Julian Pins, Simon Reilich

• Positional Determinacy with Colored Vertices: a 1-to-2-Player Lift

  Raphaël Berthon, Stéphane Le Roux

• Mean-Payoff-Parity and Lifting Strategies from MDPs to 2-Player Stochastic Games

  Richard Mayr, Mohan Sai Teja Dantam

• Generalized Bidding Games: Where Bidding and Stochastic Games Meet

  Ali Asadi, Thomas A. Henzinger, Ehsan Kafshdar Goharshady, Pavol Kebis, Kaushik Mallik

• On the Continuity of the Probabilistic Bisimilarity Distance

  Syyeda Zainab Fatmi, Stefan Kiefer, David Parker, Franck van Breugel

• On the Complexity of Robust Markov Decision Processes and Bisimulation Metrics

  Marnix Suilen, Guillermo Perez

• Reachability in Fixed-Dimensional Continuous VASS

  Michal Ajdarów, A. R. Balasubramanian, Łukasz Orlikowski

• On the Encodability of Reversible Process Calculi

  Ivan Lanese, Claudio Antares Mezzina, Iain Phillips, Irek Ulidowski, Shoji Yuen

• Sure-almost-sure and Sure-limit-sure Window Mean Payoff in Markov Decision Processes

  Pranshu Gaba, Shibashis Guha

• Minimal and Canonical Quotients for Simulation Equivalences

  Eduardo Costa Martins, Tim Willemse

• Representing One Letter Weighted Automata Over the Tropical Semiring

  Shaull Almagor, Ismaël Jecker, Filip Mazowiecki, Łukasz Orlikowski, David Purser, Henry Sinclair-Banks

• Active Diagnosis with Costs and Rewards

  Serge Haddad, Engel Lefaucheux, Stefan Schwoon

• Buffered control for opacity in timed automata

  Étienne André, Sarah Dépernet, Engel Lefaucheux

• Bisimulations and Modal Logics for Higher Dimensional Automata

  Safa Zouari, Rob van Glabbeek, Krzysztof Ziemianski

• A New Type System for Deadlock-Free Processes

  Naoki Kobayashi

  Test of Time 

• Strategy Logic

  Nir Piterman

  Test of Time 

• Reasoning About Probabilistic Loops, Moment by Moment

  Ezio Bartocci

  LiveJoint Invited FMICS Q+F 

• Category Theory for Fast Model Checking Algorithms

  Ichiro Hasuo

  LiveJoint Invited FMICS Q+F 

Q+F

• Reasoning About Probabilistic Loops, Moment by Moment

  Ezio Bartocci

  LiveJoint Invited CONCUR FMICS 

• Category Theory for Fast Model Checking Algorithms

  Ichiro Hasuo

  LiveJoint Invited CONCUR FMICS 

• QEST+FORMATS Opening

  on  Wed, 9:00 Live in  Room B

  Invited 

• Supporting Older Adults Living Independently

  Jane Hillston

  LiveInvited 

• Monitoring of Timed and Quantitative Systems

  Kim G. Larsen

  LiveInvited 

• Stationary and Transient Bounds for Nearly Lumpable or Uncertain Markov Chains

  Peter Buchholz

• Wasserstein error bounds for aggregations of continuous-time Markov chains

  Fabian Michel

• Robust Parameter Learning for Uncertain MDPs

  Yannik Schnitzer, Alessandro Abate, David Parker

• State-Space Abstractions for Parametric Timed Games

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

• Verification of parametric Markov Automata under time-bounded reachability

  Kevin van de Glind, Matthias Volk, Tim Willemse

• Learning Alternating Real-Time Automata

  Kazuki Kinoshita, Masaki Waga

• Faster algorithm for achieving minimal-size quantum decision diagrams

  Juul Sanders, Sebastiaan Brand, Tim Coopmans

• Multi-Objective Statistical Model Checking using Lightweight Strategy Sampling

  Pedro R. D'Argenio, Arnd Hartmanns, Patrick Wienhöft, Mark van Wijk

• Effective Stochastic Automata Model Checking by Interval Abstraction

  Annabell Petri, Arnd Hartmanns, Pedro D'Argenio

• Collective Decision-Making Under Timing Constraints

  Julia Klein, Tatjana Petrov

• Exact Evaluation of Probabilistic Programs with Cylindrical Algebraic Decomposition

  Mohamed Hamza Bandukara, Fredrik Dahlqvist, Niki Omidvari

• Algebraic Robust Semantics for Signal Temporal Logic with Graph Operators

  Sheryl Paul, Vidisha Kudalkar, Anand Balakrishnan, Tianhao Wu, Lars Lindemann, Jyotirmoy Deshmukh

• Scalable Reachability Analysis of Linear Continuous Systems with Property-Driven Time-Step Adaptation

  Mikkel Bjørn, Daniel Hansen, Grace Melchiors, Kim Guldstrand Larsen, Christian Schilling

• Stability Checking of Markov Jump Linear Systems via Probabilistic Temporal Logic

  Lena Becker, Holger Hermanns

• Facing the Core: State-Space Compression of Dynamic Fault Trees via PH-Distributions

  Nazareno Garagiola, Holger Hermanns

• Adaptive Importance Sampling for Static Fault Trees with Two-State Markovian Components

  Leonardo Paroli, Laura Carnevali, Enrico Vicario

• The Cost of Repetition: A Compositional Scalability Model for Attack Trees

  Clemens Fruböse, Eva Hetzel

• Stationary Analysis of Finite-Capacity M/M/1 Fork-Join Queues

  Pierre Fiorini

• The Component Queues Method for Quasi-Birth-Death Process Fitting and Analysis

  Julianna Bor, Giuliano Casale, Evgenia Smirni

• Weighing Timed Regular Languages: The Final Step

  Eugene Asarin, Aldric Degorre, Catalin Dima, Bernardo Jacobo Inclán

• Witnesses and Counterexamples for Timed Bisimulation

  Alexander Lieb, Malte Lochau

• MightyPPL: Towards model checking MTL

  Hsi-Ming Ho, S Krishna, Khushraj Madnani, Rupak Majumdar, Paritosh Pandya

• LF-mc: An Efficient Verifier for Lingua Franca

  Mario Reja, Mikheil Rukhaia, Kyungmin Bae, Mircea Marin, Peter Csaba Ölveczky

• StochasticBarrier.jl: A Toolbox for Stochastic Barrier Function Synthesis

  Rayan Mazouz, Frederik Mathiesen, Luca Laurenti, Morteza Lahijanian

FMICS

• Reducing Time to Market through Formal Methods

  Colin O'Halloran

  LiveInvited 

• Application of Formal Methods to Design and Verification of Autonomous Space Systems

  Julia Badger

  LiveInvited 

• Panel Session discussing the Industrial use of Formal Methods

  Live

• Industrial Adoption of Formal Methods: An Industry Perspective on the Transition to SPARK for Security Critical Firmware Development

  Asieh Salehi Fathabadi, Mark Hermeling

• A Formally Verified N-Dimensional Safety Shield for Autonomous Systems

  Benjamin Puyobro, Paolo Crisafulli, Burkhart Wolff

• Deductive Verification of a Patricia Trie with Creusot

  Téo Bernier, Frédéric Loulergue, Nikolai Kosmatov

• Reasoning about concurrent loops and recursion with rely-guarantee rules

  Ian J. Hayes, Larissa Meinicke, Cliff Jones

• Consistency proofs for axiomatic extensions: translating VerCors's Axiomatic Data Types into Isabelle

  Edoardo Putti, Alexander Stekelenburg

• Exploiting the Layout of a Railway Interlocking System for Path Reliability Evaluation

  Alessandro Fantechi, Gloria Gori, Jacopo Zecchi

• Lazy Three-Way Model Merging in Cinco Cloud: A Lattice-Theoretic Approach

  Jonas Schürmann, Bernhard Steffen

• Domain-Specific 3D Visualization of Formal Models

  Max Richter, Fabian Vu

• Reasoning About Probabilistic Loops, Moment by Moment

  Ezio Bartocci

  LiveJoint Invited CONCUR Q+F 

• Category Theory for Fast Model Checking Algorithms

  Ichiro Hasuo

  LiveJoint Invited CONCUR Q+F 

Express/SOS

• Expressiveness, Separation and Complexity Results on Multiparty Session Types

  Nobuko Yoshida

  Live

• On the Expressiveness of Asynchronous Processes with Nested Session Types

  Sjors Wortelboer, Dan Frumin, Jorge A. Pérez

• The MAY-preorder for timed systems with asynchronous communication

  Giovanni Bernardi, Maryline Zhang, Pedro Ribeiro

• Encoding call-by-push-value in the pi-calculus

  Hans Hüttel, Nikolaj Kristensen, Benjamin Bennetzen, Peter Steffensen

• Weighted barbed congruence

  Iwan Quémerais

• Structural Operational Semantics for String Diagrammatic Languages

  Fabio Zanasi

  Live

• The Theory of Sequential Value Passing

  Eduardo Costa Martins

• Deadlock-Free Parallel Regions for Projected Workflows

  Benedikt Bollig

• A Formal Comparison of Controllability Definitions for Deterministic and Nondeterministic Automata

  Jeroen Keiren, Michel Reniers

• Discounted-Sum Automata - Reductions between the Universality Problems

  Udi Boker

SNR

• Can We Change the Game? Reasoning about Dynamic Multi-Agent Systems

  Munyque Mittelmann

  Live

• Active Learning for the Synthesis of POMDP Policies

  Prince Mathew

  Live

• Randomised Decision Making: Expressiveness and Complexity

  James Main

  Live

• Open Problem Session

  Live

• Game Semantics for De Morgan Algebras

  Can Baskent, Andrew Lewis-Smith

• Shielding for Higher-Order Safety

  Filip Cano, Thomas A. Henzinger, Konstantin Kueffner

• Optimal MDP Repair

  Venkata Harshavardhan Chinta, Sven Schewe, Qiyi Tang, Shufang Zhu

Trends

• Ensuring Liveness Properties of Distributed Systems with Justness

  Rob van Glabbeek

  Live

• From Individual Interactions to Collective Dynamics — and Back: Why Timing Matters

  Tatjana Petrov

  Live

• Book presentation: Models of Computation based on Automata: Formal Languages and Communicating Processes

  Jos Baeten

  Live

• Abstract Operational Reasoning

  Henning Urbat

  Live

YR-CONCUR

• Invited Talk, Title TBD

  K. S. Thejaswini

  Live

• Poster Session

  Live

• Forward-Responsibility in Petri Nets

  Caroline Lemke, Heike Wehrheim

• ATCAL: a model of information manipulation by concurrent announcements

  Louwe B. Kuijer, Klara Rawska-Furman

• Simple Nash Equilibria for Qualitative Multiplayer Games

  Mona Alluwaym, Sven Schewe, James C. A. Main

• Opacity Problems in Timed Automata

  Sarah Dépernet

• Designing and Verifying a Post-Quantum Protocol using ProVerif

  Robert-William Evans, Florian Kammueller

• Duality for Horn Disjunctive Linear Relations

  Om Swostik Mishra, Christoph Haase

• Categorical Message Passing Language (CaMPL)

  Priyaa Varshinee Srinivasan, Alexanna Little Berg, Daniel K. Hashimoto

• Supporting Phased Atomicity in the OpenCL Memory Model

  Haining Tong, Keijo Heljanko

• Parallel Abstract Interpretation for Polynomial Programs with Range Bound Assertions

  Harshit Jitendra Motwani

• Sure-almost-sure and Sure-limit-sure Mean Payoff in Markov Decision Processes

  Raphaël Berthon, Pranshu Gaba, Vaani Goenka, Shibashis Guha, Chandralekha P

Test of Time

• A New Type System for Deadlock-Free Processes

  Naoki Kobayashi

  CONCUR 

• Strategy Logic

  Nir Piterman

  CONCUR