The general schedule is shown below. All times are in CEST.

Wrong password, please try again.
Registered participants can obtain access to session teasers and session zoom link by entering a password given to them by the organizers. Links to teasers and zoom session will appear when hovering above a session. Links to teasers will appear under the session or paper title.
  
You are logged in as a Qonfest participant. Hovering the mouse above a session will show more information, including links to the teaser videos. You can access the teasers for sessions or individual papers using the links in the programme below.
To join the conference, go to our gather.town session (same password as for this page).
Teasers and recording of sessions will be available on our YouTube channel

Proceedings: CONCUR • FMICS • FORMATS • QEST

Note: To enable your access to QEST papers, first click the Springer link on the QEST homepage.

Keynote Formats 12:00-13:00 Parosh Abdulla
Daniele Magazzeni Temporal Reasoning for Intelligent Financial Services: Examples and Challenges
Keynote Concur+Qest 15:45-16:45 Alessandro Abate
Boudewijn Haverkort Performance Evaluation: Model or Problem Driven?
Keynote Qest 15:45-16:45 Andrea Marin
François Baccelli Stochastic Geometry based Performance Analysis of Wireless Networks
Keynote Concur 12:00-13:00
Patricia Bouyer Parameterized concurrent games
Keynote Formats 15:45-16:45 Morteza Lahijanian
Jana Tumova Formal Methods for Robot Motion Planning with Time and Space Constraints
Keynote Concur 15:45-16:45
Davide Sangiorgi From Enhanced Coinduction towards Enhanced Induction
Opening
Closing Session
Formats Closing Session
Social Lunch
Social Lunch
Social Lunch
Concur A1 14:00-15:15 Büchi Automata Javier Esparza
Vojtěch Havlena and Ondřej Lengál Reducing (To) the Ranks: Efficient Rank-Based Büchi Automata Complementation
Kyveli Doveri, Pierre Ganty, Francesco Parolini and Francesco Ranzato Inclusion Testing of Büchi Automata Based on Well-Quasiorders
Henning Urbat, Daniel Hausmann, Stefan Milius and Lutz Schröder Nominal Büchi Automata with Name Allocation
Concur B1 14:00-15:15 Probabilistic Models Serge Haddad
Javier Esparza, Stefan Kiefer, Jan Křetínský and Maximilian Weininger Enforcing ω-Regular Properties in Markov Chains by Restarting
Stefan Kiefer, Pavel Semukhin and Cas Widdershoven Linear-Time Model Checking Branching Processes
Jakob Piribauer, Christel Baier, Nathalie Bertrand and Ocan Sankur Quantified Linear Temporal Logic over Probabilistic Systems with an Application to Vacuity Checking
Concur A2 17:00-18:15 Games 1 Patricia Bouyer
Léonard Brice, Jean-François Raskin and Marie van den Bogaard Subgame-Perfect Equilibria in Mean-Payoff Games
Mrudula Balachander, Shibashis Guha and Jean-François Raskin Fragility and Robustness in Mean-Payoff Adversarial Stackelberg Games
Alexander Kozachinskiy Continuous Positional Payoffs
Concur A3 14:00-15:15 Nondeterministic and Probabilistic Models Youssouf Oualhadj
Stefan Kiefer, Richard Mayr, Mahsa Shirmohammadi and Patrick Totzke Transience in Countable MDPs
Richard Mayr and Eric Munday Strategy Complexity of Mean Payoff, Total Payoff and Point Payoff Objectives in Countable MDPs
Ming Xu, Jingyi Mei, Ji Guan and Nengkun Yu Model Checking Quantum Continuous-Time Markov Chains
Concur B3 14:00-15:15 Distributed Systems Daniele Varacca
Benedikt Bollig, Cinzia Di Giusto, Alain Finkel, Laetitia Laversa, Etienne Lozes and Amrita Suresh A Unifying Framework for Deciding Synchronizability
Nathalie Bertrand, Bastien Thomas and Josef Widder Guard Automata for the Verification of Safety and Liveness of Distributed Algorithms
Rucha Kulkarni, Umang Mathur and Andreas Pavlogiannis Dynamic Data-Race Detection Through the Fine-Grained Lens
Concur A4 17:00-18:15 Language Theory Bernd Finkbeiner
A. R. Balasubramanian and K. S. Thejaswini Adaptive Synchronisation of Pushdown Automata
Ismaël Jecker, Nicolas Mazzocchi and Petra Wolf Decomposing Permutation Automata
Concur A5 14:00-15:15 Semantics Bartek Klin
Michele Boreale and Daniele Gorla Algebra and Coalgebra of Stream Products
Simon Foster, Chung-Kil Hur and Jim Woodock Formally Verified Simulations of State-Rich Processes Using Interaction Trees in Isabelle/HOL
Mayuko Kori, Ichiro Hasuo and Shin-ya Katsumata Fibrational Initial Algebra-Final Coalgebra Coincidence over Initial Algebras:Turning Verification Witnesses Upside Down
Concur B5 14:00-15:15 Temporal Logics and Model Checking Christel Baier
Muhammad Syifa’ul Mufid, Andrea Micheli, Alessandro Abate and Alessandro Cimatti SMT-Based Model Checking of Max-Plus Linear Systems
Florian Bruse and Martin Lange A Decidable Non-Regular Modal Fixpoint Logic
Raven Beutner and Bernd Finkbeiner A Temporal Logic for Strategic Hyperproperties
Concur A6 17:00-18:15 Games 2 Antonin Kučera
James C. A. Main, Mickael Randour and Jeremy Sproston Time Flies When Looking out of the Window: Timed Games with Window Parity Objectives
Patricia Bouyer, Youssouf Oualhadj, Mickael Randour and Pierre Vandenhove Arena-Independent Finite-Memory Determinacy in Stochastic Games
Véronique Bruyère, Jean-François Raskin and Clément Tamines Stackelberg-Pareto Synthesis
Concur A7 14:00-15:15 Dynamical Systems Aiswarya Cyriac
Christel Baier, Florian Funke, Simon Jantsch, Toghrul Karimov, Engel Lefaucheux, Florian Luca, Joël Ouaknine, David Purser, Markus A. Whiteland and James Worrell The Orbit Problem for Parametric Linear Dynamical Systems
Aneesh K. Shetty, S. Krishna and Georg Zetzsche Scope-Bounded Reachability in Valence Systems
Michal Ajdarów and Antonín Kučera Deciding Polynomial Termination Complexity for VASS Programs
Concur B7 14:00-15:15 Equivalences Yuxin Deng
Jan Friso Groote, Jan Martens and Erik de Vink Bisimulation by Partitioning Is Ω((m+n)log n)
Thorsten Wißmann, Stefan Milius and Lutz Schröder Explaining Behavioural Inequivalence Generically in Quasilinear Time
Rob van Glabbeek, Peter Höfner and Weiyou Wang Enabling Preserving Bisimulation Equivalence
Concur A8 17:00-18:15 Session Types Marco Carbone
Patrick Baillot, Alexis Ghyselen and Naoki Kobayashi Sized Types with Usages for Parallel Complexity of Pi-Calculus Processes
Rupak Majumdar, Madhavan Mukund, Felix Stutz and Damien Zufferey Generalising Projection in Asynchronous Multiparty Session Types
Simon Fowler, Wen Kokke, Ornela Dardha, Sam Lindley and J. Garrett Morris Separating Sessions Smoothly
Fmics 1 17:00-18:15 Verification Ákos Hajdu
FMICS Opening Remarks
Simon Thrane Hansen, Cláudio Gomes, Maurizio Palmieri, Casper Thule, Jaco van de Pol and Jim Woodcock Verification of Co-Simulation Algorithms Subject to Algebraic Loops and Adaptive Steps
Cláudio Belo Lourenço, Denis Cousineau, Florian Faissole, Claude Marché, David Mentré and Hiroaki Inoue Automated Verification of Temporal Properties of Ladder Programs
Maurice H. ter Beek, Vincenzo Ciancia, Diego Latella, Mieke Massink and Giorgio Oronzo Spagnolo Spatial Model Checking for Smart Stations: Research Challenges
Fmics 2 14:00-15:15 Program Safety & Education Maurice H. ter Beek
Hamid Jahanian Parametric Faults in Safety Critical Programs
Robert Rubbens, Sophie Lathouwers and Marieke Huisman Modular Transformation of Java Exceptions Modulo Errors
Bernd Westphal On Education and Training in Formal Methods for Industrial Critical Systems
Fmics 3 17:00-17:50 (Event-)B Modeling & Validation Cristina Seceleanu
Joshua Schmidt and Michael Leuschel Improving SMT Solver Integrations for the Validation of B and Event-B Models
Ismail Mendil, Yamine Ait Ameur, Neeraj Kumar Singh, Dominique Méry and Philippe Palanque Standard Conformance-by-Construction with Event-B
Fmics 4 14:00-15:15 Formal Analysis Simon Bliudze
Andrej Kiviriga, Ulrik Nyman and Kim G. Larsen Randomized Reachability Analysis in Uppaal: Fast Error Detection in Timed Systems
Baptiste Pollien, Xavier Thirioux, Christophe Garion, Gautier Hattenberger and Pierre Roux Verification of a Mathematical Library of an Autopilot with Frama-C
Davide Basile, Alessandro Fantechi and Irene Rosadi Formal Analysis of the UNISIG Safety Application Intermediate Sub-Layer
Fmics 5 17:00-18:15 Tools Anastasia Mavridou
Jens Bendisposto, David Geleßus, Michael Leuschel and Fabian Vu ProB2-UI: A Java-based User Interface for ProB
Roberto Bruttomesso Intrepid: a Scriptable and Cloud-ready SMT-based Model Checker
Daniel Larraz, Mickaël Laurent and Cesare Tinelli Merit and Blame Assignment with Kind 2
Fmics 6 18:30-19:30 Test Generation & Probabilistic Verification Dejan Nickovic
Quinn Thibeault, Jacob Anderson, Aniruddh Chandratre, Giulia Pedrielli and Georgios Fainekos PSY-TaLiRo: A Python Toolbox for Search-Based Test Generation for Cyber-Physical Systems
Riley Roberts, Benjamin Lewis, Arnd Hartmanns, Prabal Basu, Sanghamitra Roy, Koushik Chakraborty and Zhen Zhang Probabilistic Verification for Reliability of a Two-by-Two Network-on-Chip System
FMICS Closing Remarks
Formats 1 14:00-15:15 Session 1: Timed systems Hsi-Ming Ho
Thomas Mari, Thao Dang and Gregor Gössler Explaining Safety Violations in Real-Time Systems
Eugene Asarin, Thomas Ferrère, Dejan Ničković and Doğan Ulus On the complexity of timed pattern matching
Formats 2 17:00-18:15 Invited Presentations 1: Timed automata Krishna S
Damien Busatto-Gaston, Benjamin Monmege, Pierre-Alain Reynier and Ocan Sankur Robust Controller Synthesis in Timed Büchi Automata: A Symbolic Approach
Kim G. Larsen, Marius Mikučionis, Marco Muñiz and Jiří Srba Urgent Partial Order Reduction for Extended Timed Automata
Formats 3 14:00-15:15 Special Session 1: Synthesis and control Igor Potapov
Jun Liu Closing the Gap between Discrete Abstractions and Continuous Control: Completeness via Robustness and Controllability
Andrea Peruffo and Alessandro Abate Formal Abstraction and Synthesis of Parametric Stochastic Processes
Formats 4 17:00-17:50 Invited Presentations 2: Timed games Engel Lefaucheux
Thomas Brihaye, Aline Goeminne On Subgame Perfect Equilibria in Turn-Based Reachability Timed Games
Lorenzo Clemente, Sławomir Lasota, Radosław Piórkowski Timed Games and Deterministic Separability
Formats 5 14:00-15:15 Session 2: Verification of timed systems Mickael Randour
Sebastian Lund, Kim G. Larsen, Marco Muñiz, Jesper A. van Diepen, Tobias R. Jørgensen and Tobias S. Andersen An Integer Static Analysis for Better Extrapolation in Uppaal
Frederik Meyer Bønneland, Peter Gjøl Jensen, Kim G. Larsen, Marco Muñiz and Jiří Srba Stubborn Set Reduction for Timed Reachability and Safety Games
Formats 6 17:00-18:15 Special Session 2: Verification of nonlinear systems Sadegh Soudjani
Edward Kim, Stanley Bak and Parasara Sridhar Duggirala Automatic Dynamic Parallelotope Bundles for Reachability Analysis of Nonlinear Systems
Sara Mohammadinejad, Brandon Paulsen, Jyotirmoy V. Deshmukh and Chao Wang DiffRNN: Differential verification of Recurrent Neural Networks
FORMATS closing session
Qest 1 14:00-15:15 Probabilistic Model Checking Gethin Norman
Michaela Klauck and Holger Hermanns A Modest Approach to Dynamic Heuristic Search in Probabilistic Model Checking
Arnd Hartmanns, Joost-Pieter Katoen, Bram Kohlen and Jip Spel Tweaking the Odds in Probabilistic Timed Automata
Samuel Teuber and Alexander Weigl Quantifying Software Reliability via Model-Counting
Qest 2 17:00-18:15 Quantitative Models and Metamodels: Analysis and Validation Sabina Rossi
Laura Carnevali, Marco Paolieri, Riccardo Reali and Enrico Vicario Compositional safe approximation of response time distribution of complex workflows
Stefan Kaalen, Mattias Nyberg and Olle Mattsson Transient Analysis of Hierarchical Semi-Markov Process Models with Tool Support in Stateflow
Michael Rausch and William Sanders Evaluating the Effectiveness of Metamodels in Emulating Quantitative Models
Qest 3 11:45-13:00 Queueing Systems Tadeusz Czachorski
Alexander Scheffler and Steffen Bondorf Network Calculus for Bounding Delays in Feedforward Networks of FIFO Queueing Systems
Maryam Akbari-Moghaddam and Douglas G. Down SEH: Size Estimate Hedging for Single-Server Queues
Bogdan Ghit and Asser Tantawi An Approximate Bribe Queueing Model for Bid Advising in Cloud Spot Markets
Qest 4 14:00-15:15 Learning and Verification David Parker
Timo P. Gros, Daniel Höller, Jörg Hoffmann, Michaela Klauck, Hendrik Meerkamp and Verena Wolf DSMC Evaluation Stages: Fostering Robust and Safe Behavior in Deep Reinforcement Learning
Paul Piho and Jane Hillston Active and sparse methods in smoothed model checking
Damien Busatto-Gaston, Debraj Chakraborty, Shibashis Guha, Guillermo Perez and Jean-François Raskin Safe Learning for Near-Optimal Scheduling
Qest 5 17:00-17:50 Simulation Anne Remke
Rebecca Haehn, Erika Abraham and Nils Nießen Symbolic Simulation of Railway Timetables under Consideration of Stochastic Dependencies
Marco Gribaudo, Daniele Manini and Mauro Iacono Simulation of n-dimensional second-order fluid models with different absorbing, reflecting and mixed barriers
Qest 6 14:00-15:15 Performance Evaluation Marco Gribaudo
Murray Woodside Queue Response Times with Server Speed Controlled by Measured Utilizations
Runan Wang, Giuliano Casale and Antonio Filieri Service Demand Distribution Estimation for Microservices Using Markovian Arrival Processes
Grzegorz Kielanski and Benny Van Houdt Performance analysis of work stealing strategies in large scale multi-threaded computing
Qest 7 17:00-18:15 Abstractions and Aggregations Laura Carnevali
Michael Backenköhler, Luca Bortolussi, Gerrit Großmann and Verena Wolf Stationary Distribution Approximations of Markovian Population Models using Aggregation
Carla Piazza, Sabina Rossi Reasoning about Proportional Lumpability
Luca Cardelli, Radu Grosu, Kim G. Larsen, Mirco Tribastone, Max Tschaikowski and Andrea Vandin Lumpability for Uncertain Continuous-Time Markov Chains
Qest 8 18:30-19:30 Stochastic Models Verena Wolf
Engel Lefaucheux Approximate Diagnosis of Controllable Stochastic Systems Accurate Approximate Diagnosis of (Controllable) Stochastic Systems
Carina Pilch, Stefan Schupp and Anne Remke Optimizing reachability probabilities for a restricted class of Stochastic Hybrid Automata via Flowpipe-Construction
Christina Kolb, Carlos Budde and Mariëlle Stoelinga Attack Trees vs. Fault Trees: two sides of the same coin from different currencies
Express/SOS Invited Talk 1 09:00-10:00 Valentina Castiglioni
Jan Friso Groote Infinite choice and probability distributions. An open problem: The real hotel
Express/SOS 2 10:30-12:00 Jurriaan Rot
Xian Xu and Wenbo Zhang On Decidability of the Bisimilarity on Higher-order Processes with Parameterization
Benjamin Bisping and Luisa Montanari A Game Characterisation for Contrasimilarity
Eric Alsmann, Florian Bruse and Martin Lange Separating the Expressive Power of Propositional Dynamic and Modal Fixpoint Logics
Express/SOS Invited Talk 2 13:00-14:00 Silvia Ghilezan
Dave Parker Probabilistic Verification of Concurrent Autonomous Systems
Express/SOS 3 14:00-15:00 Silvia Ghilezan
Alen Arslanagic, Anda-Amelia Palamariuc and Jorge A. Pérez Minimal session types for the pi-calculus
Manfred Schmidt-Schauss and David Sabel Minimal Translations from Synchronous Communication to Synchronizing Locks
Express/SOS Invited Talk 3 15:30-16:30 Ornela Dardha
Amal Ahmed Semantic Soundness for Language Interoperability
Express/SOS 4 16:30-17:00 Ornela Dardha
Matteo Cimini and Benjamin Mourad Language Transformations in the Classroom
SNR 1 14:50-15:30
T. Badings, A. Abate, N. Jansen, D. Parker, H. Poonawala, M. Stoelinga Sampling-Based Robust Control of Autonomous Systems with Non-Gaussian noise
N. Pal, T.T. Johnson Safety and Robustness Verification of Autoencoder based Regression Model using NNV Tool
SNR Invited Talk 2 15:45-16:35
Bardh Hoxha Autonomous CPS: Verification and Control
SNR 2 16:35-16:55
D. Grundt, S. Liviu Jurj, W. Hagemann, P. Kröger, M. Fränzle Verification of Sigmoidal Artificial Neural Networks using iSAT
SNR Invited Talk 3 17:00-17:50
Nils Jansen Safe Planning under Epistemic Uncertainty and Partial Information
SNR 3 17:50-18:15
W. Haddad, L. Nguyen, T.T. Johnson Model Checking for Rectangular Hybrid Systems: A Quantified Encoding Approach
Trends Invited Talk 1 14:15-15:15
Christel Baier From verification to causality-based explications
Trends Invited Talk 2 15:45-16:45
Alexey Gotsman Rigorous Design of Atomic Transaction Commit Protocols
Trends Invited Talk 3 17:00-18:00
Ilaria Castellani Event structure semantics for asynchronous multiparty sessions
PM 1 14:00-15:15 PM deployment on large-stack systems
Alessandro Abate Predictive maintenance for Smart Buildings
Lisandro A. Jimenez-Roa System-level prognostics for management of complex assets: Opportunities and Challenges
Nick Oosterhof Detecting HVAC cooling malfunctions in trains
PM 2 15:45-16:45 Data- and ML-based approaches to PM
Kim G. Larsen Predictive Maintenance of COVID-19
Jaap van Ekris Maintaining sleeping giants, using quantitative data to optimise system maintenance
PM 3 17:00-18:15 Boundaries and new promises of PM
Roberto Manuel Cibils and Leonardo Diamonte Use of Monte Carlo for predicting the failure rate of leading edge CMOS integrated circuits
Alessandro Cimatti An interdisciplinary approach to predictive maintenance