Program by Day

I0		CONCUR (Room A)

8:30		On now Registration & Coffee





9:00		On now Word Automata with Limited Nondeterminism Session chair: Patrick Totzke Qiyi Tang CONCUR











10:00		On now Coffee Break





10:30		On now CONCUR Session 1 - Stochastic Games & MDPs I Session chair: Pedro R. D'Argenio Asymmetrically-Discounted Stochastic GamesSarvin Bahmani, Soumyajit Paul, Sven Schewe, Shadi Tasdighi Kalat, Ashutosh Trivedi Probabilistic Model Checking via Families of Deterministic and Unambiguous Finite AutomataChristel Baier, Sascha Klüppelholz, Timm Spork Positional Determinacy with Colored Vertices: a 1-to-2-Player LiftRaphaël Berthon, Stéphane Le Roux Mean-Payoff-Parity and Lifting Strategies from MDPs to 2-Player Stochastic GamesRichard Mayr, Mohan Sai Teja Dantam

















12:00		On now Lunch

















13:30		On now CONCUR Session 2 - Stochastic Games & MDPs II Session chair: Nathalie Bertrand Generalized Bidding Games: Where Bidding and Stochastic Games MeetAli Asadi, Thomas A. Henzinger, Ehsan Kafshdar Goharshady, Pavol Kebis, Kaushik Mallik Sure-almost-sure and Sure-limit-sure Window Mean Payoff in Markov Decision ProcessesPranshu Gaba, Shibashis Guha PAC Learning in Turn-Based Stochastic Games with Reachability Objectives: A Decentralized Private Approach via Expected Conditional DistanceAli Asadi, Krishnendu Chatterjee, Pavol Kebis













14:40		On now Coffee Break



15:00		On now CONCUR Session 3 - Behavioural Metrics Session chair: Jurriaan Rot Threshold-Based Behavioural DistancesJonas Forster, Lutz Schröder, Paul Wild, Barbara König, Pedro Nora On the Continuity of the Probabilistic Bisimilarity DistanceSyyeda Zainab Fatmi, Stefan Kiefer, David Parker, Franck van Breugel On the Complexity of Robust Markov Decision Processes and Bisimulation MetricsMarnix Suilen, Guillermo Perez













16:10		On now Coffee Break



16:30		On now CONCUR Session 4 - (Bi)Simulations Session chair: Rob van Glabbeek Revisiting True Concurrency Bisimilarities: On the Role of Backward Ready Multisets and Why They Are Not Enough for HPB and HHPBAndrea Esposito, Marco Bernardo Wheeler BisimulationsNicola Cotumaccio Minimal and Canonical Quotients for Simulation EquivalencesEduardo Costa Martins, Tim Willemse













17:40

CONCUR (Room A)

8:30	On now Registration & Coffee
9:00	On now Word Automata with Limited Nondeterminism Session chair: Patrick Totzke Qiyi Tang CONCUR
10:00	On now Coffee Break
10:30	On now CONCUR Session 1 - Stochastic Games & MDPs I Session chair: Pedro R. D'Argenio Asymmetrically-Discounted Stochastic Games Sarvin Bahmani, Soumyajit Paul, Sven Schewe, Shadi Tasdighi Kalat, Ashutosh Trivedi Probabilistic Model Checking via Families of Deterministic and Unambiguous Finite Automata Christel Baier, Sascha Klüppelholz, Timm Spork 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
12:00	On now Lunch
13:30	On now CONCUR Session 2 - Stochastic Games & MDPs II Session chair: Nathalie Bertrand Generalized Bidding Games: Where Bidding and Stochastic Games Meet Ali Asadi, Thomas A. Henzinger, Ehsan Kafshdar Goharshady, Pavol Kebis, Kaushik Mallik Sure-almost-sure and Sure-limit-sure Window Mean Payoff in Markov Decision Processes Pranshu Gaba, Shibashis Guha PAC Learning in Turn-Based Stochastic Games with Reachability Objectives: A Decentralized Private Approach via Expected Conditional Distance Ali Asadi, Krishnendu Chatterjee, Pavol Kebis
14:40	On now Coffee Break
15:00	On now CONCUR Session 3 - Behavioural Metrics Session chair: Jurriaan Rot Threshold-Based Behavioural Distances Jonas Forster, Lutz Schröder, Paul Wild, Barbara König, Pedro Nora 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
16:10	On now Coffee Break
16:30	On now CONCUR Session 4 - (Bi)Simulations Session chair: Rob van Glabbeek 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 Wheeler Bisimulations Nicola Cotumaccio Minimal and Canonical Quotients for Simulation Equivalences Eduardo Costa Martins, Tim Willemse

18:00		On now Reception

CONCUR (Room A)

18:00	On now Reception

Caption

Invited

CONCUR

I0		CONCUR (Room A)		QEST+FORMATS (Room B)

8:30	On now Registration & Coffee





9:00	On now CONCUR Session 5 - Vector Addition Systems Session chair: Shaull Almagor Reachability in Fixed-Dimensional Continuous VASSMichal Ajdarów, A. R. Balasubramanian, Łukasz Orlikowski Monadic Presburger Predicates have Robust Population ProtocolsPhilipp Czerner, Javier Esparza, Vincent Fischer, Roland Guttenberg, Julian Pins, Simon Reilich Improving Reachability in Vector Addition Systems through PumpabilityWeijun Chen, Yuxi Fu, Yangluo Zheng	On now QEST+FORMATS Opening Session chair: Mingshuai Chen & Max Tschaikowski Q+F

9:10		On now Monitoring of Timed and Quantitative Systems Session chair: Mingshuai Chen Kim G. Larsen Q+F











10:10	On now Coffee Break



10:30	On now CONCUR Session 6 - Concurrency and Verification Session chair: Jérémy Ledent Prophecy-Based Automated Verification of Message-Passing ProgramsTakashi Nagatomi, Musashi Katsura, Naoki Kobayashi, Yusuke Matsushita, Ken Sakayori An MSO Framework for Weak-Memory Verification and RobustnessGiovanna Kobus Conrado, Andreas Pavlogiannis when Behaviours Have to Happen: An Axiomatic Model of Causality in Behaviour-Oriented ConcurrencyLuke Cheeseman, Elias Castegren, Tobias Wrigstad, Sophia Drossopoulou, Matthew Parkinson On the Encodability of Reversible Process CalculiIvan Lanese, Claudio Antares Mezzina, Iain Phillips, Irek Ulidowski, Shoji Yuen	On now Q+F Session 1 - Markov Models under Uncertainty Session chair: Martin Fränzle Stationary and Transient Bounds for Nearly Lumpable or Uncertain Markov ChainsPeter Buchholz Wasserstein error bounds for aggregations of continuous-time Markov chainsFabian Michel Robust Parameter Learning for Uncertain MDPsYannik Schnitzer, Alessandro Abate, David Parker

















12:00	On now Lunch

















13:30	On now CONCUR Session 7 - Time Session chair: Tom Henzinger Reaching as Cheap as Possible in 1-clock Robust Weighted Timed GamesNathalie Bertrand, Maëlle Gautrin, Julie Parreaux Buffered control for opacity in timed automataÉtienne André, Sarah Dépernet, Engel Lefaucheux Positional Properties in Temporal LogicJessica Newman, Benjamin Plummer	On now Supporting Older Adults Living Independently Session chair: Andrea Vandin Jane Hillston Q+F











14:30		On now Coffee Break

14:40	On now Coffee Break



15:00	On now CONCUR Test of Time Session Session chair: Wan Fokkink A New Type System for Deadlock-Free ProcessesNaoki Kobayashi Strategy LogicNir Piterman	On now Q+F Session 2 - Parametric Games and Automata Session chair: Masaki Waga State-Space Abstractions for Parametric Timed GamesMikael Bisgaard Dahlsen-Jensen, Jaco van de Pol, Laure Petrucci Verification of parametric Markov Automata under time-bounded reachabilityKevin van de Glind, Matthias Volk, Tim Willemse











16:00		On now Coffee Break

16:10	On now Coffee Break



16:30	On now CONCUR Session 8 - Higher Dimensional Automata and Semantics Session chair: Sergey Goncharov Bisimulations and Modal Logics for Higher Dimensional AutomataSafa Zouari, Rob van Glabbeek, Krzysztof Ziemianski Algebraic Characterization of FO-definable Languages of Higher-Dimensional AutomataEnzo Erlich, Jérémy Ledent, Krzysztof Ziemiański Concurrent Visibility: higher-order concurrency with first-order storeIwan Quémerais, Guilhème Jaber, Ken Sakayori, Davide Sangiorgi	On now Q+F Session 3 - Learning and Quantum Systems Session chair: Kim G. Larsen Learning Alternating Real-Time AutomataKazuki Kinoshita, Masaki Waga Faster algorithm for achieving minimal-size quantum decision diagramsJuul Sanders, Sebastiaan Brand, Tim Coopmans













17:40

CONCUR (Room A)

8:30	On now Registration & Coffee
9:00	On now CONCUR Session 5 - Vector Addition Systems Session chair: Shaull Almagor Reachability in Fixed-Dimensional Continuous VASS Michal Ajdarów, A. R. Balasubramanian, Łukasz Orlikowski Monadic Presburger Predicates have Robust Population Protocols Philipp Czerner, Javier Esparza, Vincent Fischer, Roland Guttenberg, Julian Pins, Simon Reilich Improving Reachability in Vector Addition Systems through Pumpability Weijun Chen, Yuxi Fu, Yangluo Zheng
10:10	On now Coffee Break
10:30	On now CONCUR Session 6 - Concurrency and Verification Session chair: Jérémy Ledent Prophecy-Based Automated Verification of Message-Passing Programs Takashi Nagatomi, Musashi Katsura, Naoki Kobayashi, Yusuke Matsushita, Ken Sakayori An MSO Framework for Weak-Memory Verification and Robustness Giovanna Kobus Conrado, Andreas Pavlogiannis when Behaviours Have to Happen: An Axiomatic Model of Causality in Behaviour-Oriented Concurrency Luke Cheeseman, Elias Castegren, Tobias Wrigstad, Sophia Drossopoulou, Matthew Parkinson On the Encodability of Reversible Process Calculi Ivan Lanese, Claudio Antares Mezzina, Iain Phillips, Irek Ulidowski, Shoji Yuen
12:00	On now Lunch
13:30	On now CONCUR Session 7 - Time Session chair: Tom Henzinger Reaching as Cheap as Possible in 1-clock Robust Weighted Timed Games Nathalie Bertrand, Maëlle Gautrin, Julie Parreaux Buffered control for opacity in timed automata Étienne André, Sarah Dépernet, Engel Lefaucheux Positional Properties in Temporal Logic Jessica Newman, Benjamin Plummer
14:40	On now Coffee Break
15:00	On now CONCUR Test of Time Session Session chair: Wan Fokkink A New Type System for Deadlock-Free Processes Naoki Kobayashi Strategy Logic Nir Piterman
16:10	On now Coffee Break
16:30	On now CONCUR Session 8 - Higher Dimensional Automata and Semantics Session chair: Sergey Goncharov Bisimulations and Modal Logics for Higher Dimensional Automata Safa Zouari, Rob van Glabbeek, Krzysztof Ziemianski Algebraic Characterization of FO-definable Languages of Higher-Dimensional Automata Enzo Erlich, Jérémy Ledent, Krzysztof Ziemiański Concurrent Visibility: higher-order concurrency with first-order store Iwan Quémerais, Guilhème Jaber, Ken Sakayori, Davide Sangiorgi

QEST+FORMATS (Room B)

8:30	On now Registration & Coffee
9:00	On now QEST+FORMATS Opening Session chair: Mingshuai Chen & Max Tschaikowski Q+F
9:10	On now Monitoring of Timed and Quantitative Systems Session chair: Mingshuai Chen Kim G. Larsen Q+F
10:10	On now Coffee Break
10:30	On now Q+F Session 1 - Markov Models under Uncertainty Session chair: Martin Fränzle 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
12:00	On now Lunch
13:30	On now Supporting Older Adults Living Independently Session chair: Andrea Vandin Jane Hillston Q+F
14:30	On now Coffee Break
15:00	On now Q+F Session 2 - Parametric Games and Automata Session chair: Masaki Waga 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
16:00	On now Coffee Break
16:30	On now Q+F Session 3 - Learning and Quantum Systems Session chair: Kim G. Larsen Learning Alternating Real-Time Automata Kazuki Kinoshita, Masaki Waga Faster algorithm for achieving minimal-size quantum decision diagrams Juul Sanders, Sebastiaan Brand, Tim Coopmans

Caption

Invited

CONCUR

Q+F

I0		CONCUR (Room A)		QEST+FORMATS (Room B)		FMICS (Room D)

8:30	On now Registration & Coffee





9:00	On now Reasoning About Probabilistic Loops, Moment by Moment Session chair: Max Tschaikowski Ezio Bartocci Joint Room A











10:00	On now Coffee Break





10:30	On now CONCUR Session 9 - Algebraic Methods Session chair: Lutz Schröder Compositionality in Coalgebraic Trace SemanticsRobin Jourde, Henning Urbat, Sergey Goncharov, Stelios Tsampas, Jonas Forster GKAT with Hoare HypothesesJurriaan Rot, Todd Schmid, Jana Wagemaker Continuous Algebras with HypothesesLukas Mulder, Damien Pous, Jana Wagemaker Coinductive reasoning for parametrized functors and monadsUgo Dal Lago, Zeinab Galal	On now Q+F Session 4 - Stochastic Model Checking Session chair: Peter Buchholz Multi-Objective Statistical Model Checking using Lightweight Strategy SamplingPedro R. D'Argenio, Arnd Hartmanns, Patrick Wienhöft, Mark van Wijk Effective Stochastic Automata Model Checking by Interval AbstractionAnnabell Petri, Arnd Hartmanns, Pedro D'Argenio Collective Decision-Making Under Timing ConstraintsJulia Klein, Tatjana Petrov	On now FMICS Session 1 - Formal Verification Session chair: Alessandro Fantechi Industrial Adoption of Formal Methods: An Industry Perspective on the Transition to SPARK for Security Critical Firmware DevelopmentAsieh Salehi Fathabadi, Mark Hermeling A Formally Verified N-Dimensional Safety Shield for Autonomous SystemsBenjamin Puyobro, Paolo Crisafulli, Burkhart Wolff Deductive Verification of a Patricia Trie with CreusotTéo Bernier, Frédéric Loulergue, Nikolai Kosmatov

















12:00	On now Lunch

















13:30	On now CONCUR Session 10 - Parameterised Verification Session chair: Dmitry Chistikov WinPop: Making populations win togetherNathalie Bertrand, Patricia Bouyer, Luc Lapointe, Corto Mascle Parameterized Verification of Asynchronous Round-Based Distributed Algorithms via Reduction to Finite-Counter SystemsNathalie Bertrand, Pranav Ghorpade, Sasha Rubin On parameterized verification over tree topologiesRomain Delpy, Anca Muscholl, Grégoire Sutre	On now Q+F Session 5 - Probabilistic and Temporal Logic Semantics Session chair: Jane Hillston Exact Evaluation of Probabilistic Programs with Cylindrical Algebraic DecompositionMohamed Hamza Bandukara, Fredrik Dahlqvist, Niki Omidvari Algebraic Robust Semantics for Signal Temporal Logic with Graph OperatorsSheryl Paul, Vidisha Kudalkar, Anand Balakrishnan, Tianhao Wu, Lars Lindemann, Jyotirmoy Deshmukh	On now Application of Formal Methods to Design and Verification of Autonomous Space Systems Session chair: Kristin-Yvonne Rozier Julia Badger FMICS











14:30		On now Coffee Break

14:40	On now Coffee Break		On now Coffee Break



15:00	On now An Introduction to Multi-Environment Markov Decision Processes Session chair: Patrick Totzke Jean-François Raskin CONCUR	On now Q+F Session 6 - Continuous and Hybrid Systems Session chair: Tatjana Petrov Scalable Reachability Analysis of Linear Continuous Systems with Property-Driven Time-Step AdaptationMikkel Bjørn, Daniel Hansen, Grace Melchiors, Kim Guldstrand Larsen, Christian Schilling Stability Checking of Markov Jump Linear Systems via Probabilistic Temporal LogicLena Becker, Holger Hermanns	On now FMICS Session 2 - Advanced Reasoning Session chair: Martin Georg Fränzle Reasoning about concurrent loops and recursion with rely-guarantee rulesIan J. Hayes, Larissa Meinicke, Cliff Jones Consistency proofs for axiomatic extensions: translating VerCors's Axiomatic Data Types into IsabelleEdoardo Putti, Alexander Stekelenburg











16:00

CONCUR (Room A)

8:30	On now Registration & Coffee
9:00	On now Reasoning About Probabilistic Loops, Moment by Moment Session chair: Max Tschaikowski Ezio Bartocci Joint Room A
10:00	On now Coffee Break
10:30	On now CONCUR Session 9 - Algebraic Methods Session chair: Lutz Schröder Compositionality in Coalgebraic Trace Semantics Robin Jourde, Henning Urbat, Sergey Goncharov, Stelios Tsampas, Jonas Forster GKAT with Hoare Hypotheses Jurriaan Rot, Todd Schmid, Jana Wagemaker Continuous Algebras with Hypotheses Lukas Mulder, Damien Pous, Jana Wagemaker Coinductive reasoning for parametrized functors and monads Ugo Dal Lago, Zeinab Galal
12:00	On now Lunch
13:30	On now CONCUR Session 10 - Parameterised Verification Session chair: Dmitry Chistikov 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 On parameterized verification over tree topologies Romain Delpy, Anca Muscholl, Grégoire Sutre
14:40	On now Coffee Break
15:00	On now An Introduction to Multi-Environment Markov Decision Processes Session chair: Patrick Totzke Jean-François Raskin CONCUR

QEST+FORMATS (Room B)

8:30	On now Registration & Coffee
9:00	On now Reasoning About Probabilistic Loops, Moment by Moment Session chair: Max Tschaikowski Ezio Bartocci Joint Room A
10:00	On now Coffee Break
10:30	On now Q+F Session 4 - Stochastic Model Checking Session chair: Peter Buchholz 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
12:00	On now Lunch
13:30	On now Q+F Session 5 - Probabilistic and Temporal Logic Semantics Session chair: Jane Hillston 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
14:30	On now Coffee Break
15:00	On now Q+F Session 6 - Continuous and Hybrid Systems Session chair: Tatjana Petrov 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

FMICS (Room D)

8:30	On now Registration & Coffee
9:00	On now Reasoning About Probabilistic Loops, Moment by Moment Session chair: Max Tschaikowski Ezio Bartocci Joint Room A
10:00	On now Coffee Break
10:30	On now FMICS Session 1 - Formal Verification Session chair: Alessandro Fantechi 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
12:00	On now Lunch
13:30	On now Application of Formal Methods to Design and Verification of Autonomous Space Systems Session chair: Kristin-Yvonne Rozier Julia Badger FMICS
14:40	On now Coffee Break
15:00	On now FMICS Session 2 - Advanced Reasoning Session chair: Martin Georg Fränzle 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

19:00		On now Social Dinner & Cruise (Boarding at 7:15pm)

CONCUR (Room A)

19:00	On now Social Dinner & Cruise (Boarding at 7:15pm)

QEST+FORMATS (Room B)

19:00	On now Social Dinner & Cruise (Boarding at 7:15pm)

FMICS (Room D)

19:00	On now Social Dinner & Cruise (Boarding at 7:15pm)

Caption

Invited

CONCUR

Q+F

FMICS

I0		CONCUR (Room A)		QEST+FORMATS (Room B)		FMICS (Room D)

8:30	On now Registration & Coffee





9:00	On now Category Theory for Fast Model Checking Algorithms Session chair: Ana Sokolova Ichiro Hasuo Joint Room A











10:00	On now Coffee Break





10:30	On now CONCUR Session 11 - Quantitative Verification Session chair: Jean-François Raskin Monitoring Discounted Sum PropertiesFilip Cano, Thomas A. Henzinger, Konstantin Kueffner, Ege Saraç Completeness for Probabilistic Boolean TapesFilippo Bonchi, Cipriano Junior Cioffo Graded Semantics of Nominal SystemsHannes Schulze, Lutz Schröder, Üsame Cengiz Representing One Letter Weighted Automata Over the Tropical SemiringShaull Almagor, Ismaël Jecker, Filip Mazowiecki, Łukasz Orlikowski, David Purser, Henry Sinclair-Banks	On now Q+F Session 7 - Dependability and Security Analysis Session chair: Arnd Hartmanns Facing the Core: State-Space Compression of Dynamic Fault Trees via PH-DistributionsNazareno Garagiola, Holger Hermanns Adaptive Importance Sampling for Static Fault Trees with Two-State Markovian ComponentsLeonardo Paroli, Laura Carnevali, Enrico Vicario The Cost of Repetition: A Compositional Scalability Model for Attack TreesClemens Fruböse, Eva Hetzel	On now FMICS Session 3 - Advanced Analysis Session chair: Maurice ter Beek Exploiting the Layout of a Railway Interlocking System for Path Reliability EvaluationAlessandro Fantechi, Gloria Gori, Jacopo Zecchi Lazy Three-Way Model Merging in Cinco Cloud: A Lattice-Theoretic ApproachJonas Schürmann, Bernhard Steffen Domain-Specific 3D Visualization of Formal ModelsMax Richter, Fabian Vu

















12:00	On now Lunch

















13:30	On now CONCUR Session 12 - Automata and Decompositions Session chair: Anca Muscholl Decomposition of Automata recognizing IdealsMathias Berry, Ismaël Jecker, Pierre-Cyrille Héam A Factorization Theorem for Forest AlgebrasShaull Almagor, Michaël Cadilhac, Asaf Shoham Complementing Emerson-Lei Elevator AutomataOndrej Alexaj, Vojtěch Havlena, Ondřej Lengál, Yong Li, Nicolas Mazzocchi	On now Q+F Session 8 - Queueing and Performance Models Session chair: Enrico Vicario Stationary Analysis of Finite-Capacity M/M/1 Fork-Join QueuesPierre Fiorini The Component Queues Method for Quasi-Birth-Death Process Fitting and AnalysisJulianna Bor, Giuliano Casale, Evgenia Smirni	On now Reducing Time to Market through Formal Methods Session chair: Peter Gorm Larsen Colin O'Halloran FMICS











14:30		On now Coffee Break

14:40	On now Coffee Break		On now Coffee Break



15:00	On now CONCUR Session 13 - Partial Observation Session chair: Sven Schewe Active Diagnosis with Costs and RewardsSerge Haddad, Engel Lefaucheux, Stefan Schwoon From Coalgebraic Determinization to Belief Construction for Partial ObservabilityMayuko Kori, Kazuki Watanabe Classification under uncertaintyOfer Leshkowitz, Orna Kupferman	On now Q+F Session 9 - Timed Automata and Languages Session chair: Marco Bernardo Weighing Timed Regular Languages: The Final StepEugene Asarin, Aldric Degorre, Catalin Dima, Bernardo Jacobo Inclán Witnesses and Counterexamples for Timed BisimulationAlexander Lieb, Malte Lochau	On now Panel Session discussing the Industrial use of Formal Methods Session chair: Peter Gorm Larsen (moderator) Peter Gorm Larsen (moderator), Maurice ter Beek, Julia Badger, Colin O'Halloran











16:00		On now Coffee Break

16:10	On now Coffee Break



16:30		On now Q+F Session 10 - Verification Tools Session chair: Eugene Asarin MightyPPL: Towards model checking MTLHsi-Ming Ho, S Krishna, Khushraj Madnani, Rupak Majumdar, Paritosh Pandya LF-mc: An Efficient Verifier for Lingua FrancaMario Reja, Mikheil Rukhaia, Kyungmin Bae, Mircea Marin, Peter Csaba Ölveczky StochasticBarrier.jl: A Toolbox for Stochastic Barrier Function SynthesisRayan Mazouz, Frederik Mathiesen, Luca Laurenti, Morteza Lahijanian











17:30

CONCUR (Room A)

8:30	On now Registration & Coffee
9:00	On now Category Theory for Fast Model Checking Algorithms Session chair: Ana Sokolova Ichiro Hasuo Joint Room A
10:00	On now Coffee Break
10:30	On now CONCUR Session 11 - Quantitative Verification Session chair: Jean-François Raskin Monitoring Discounted Sum Properties Filip Cano, Thomas A. Henzinger, Konstantin Kueffner, Ege Saraç Completeness for Probabilistic Boolean Tapes Filippo Bonchi, Cipriano Junior Cioffo Graded Semantics of Nominal Systems Hannes Schulze, Lutz Schröder, Üsame Cengiz Representing One Letter Weighted Automata Over the Tropical Semiring Shaull Almagor, Ismaël Jecker, Filip Mazowiecki, Łukasz Orlikowski, David Purser, Henry Sinclair-Banks
12:00	On now Lunch
13:30	On now CONCUR Session 12 - Automata and Decompositions Session chair: Anca Muscholl Decomposition of Automata recognizing Ideals Mathias Berry, Ismaël Jecker, Pierre-Cyrille Héam A Factorization Theorem for Forest Algebras Shaull Almagor, Michaël Cadilhac, Asaf Shoham Complementing Emerson-Lei Elevator Automata Ondrej Alexaj, Vojtěch Havlena, Ondřej Lengál, Yong Li, Nicolas Mazzocchi
14:40	On now Coffee Break
15:00	On now CONCUR Session 13 - Partial Observation Session chair: Sven Schewe Active Diagnosis with Costs and Rewards Serge Haddad, Engel Lefaucheux, Stefan Schwoon From Coalgebraic Determinization to Belief Construction for Partial Observability Mayuko Kori, Kazuki Watanabe Classification under uncertainty Ofer Leshkowitz, Orna Kupferman
16:10	On now Coffee Break

QEST+FORMATS (Room B)

8:30	On now Registration & Coffee
9:00	On now Category Theory for Fast Model Checking Algorithms Session chair: Ana Sokolova Ichiro Hasuo Joint Room A
10:00	On now Coffee Break
10:30	On now Q+F Session 7 - Dependability and Security Analysis Session chair: Arnd Hartmanns 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
12:00	On now Lunch
13:30	On now Q+F Session 8 - Queueing and Performance Models Session chair: Enrico Vicario 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
14:30	On now Coffee Break
15:00	On now Q+F Session 9 - Timed Automata and Languages Session chair: Marco Bernardo 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
16:00	On now Coffee Break
16:30	On now Q+F Session 10 - Verification Tools Session chair: Eugene Asarin 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 (Room D)

8:30	On now Registration & Coffee
9:00	On now Category Theory for Fast Model Checking Algorithms Session chair: Ana Sokolova Ichiro Hasuo Joint Room A
10:00	On now Coffee Break
10:30	On now FMICS Session 3 - Advanced Analysis Session chair: Maurice ter Beek 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
12:00	On now Lunch
13:30	On now Reducing Time to Market through Formal Methods Session chair: Peter Gorm Larsen Colin O'Halloran FMICS
14:40	On now Coffee Break
15:00	On now Panel Session discussing the Industrial use of Formal Methods Session chair: Peter Gorm Larsen (moderator) Peter Gorm Larsen (moderator), Maurice ter Beek, Julia Badger, Colin O'Halloran

18:00		On now Football

CONCUR (Room A)

18:00	On now Football

QEST+FORMATS (Room B)

18:00	On now Football

FMICS (Room D)

18:00	On now Football

Caption

Invited

CONCUR

Q+F

FMICS

I0		EXPRESS/SOS (Room B)		SNR (Room C)		Trends (Room D)		YR-CONCUR (G-FLEX)

8:30	On now Registration & Coffee





9:00	On now Expressiveness, Separation and Complexity Results on Multiparty Session Types Nobuko Yoshida	On now Can We Change the Game? Reasoning about Dynamic Multi-Agent Systems Munyque Mittelmann	On now Ensuring Liveness Properties of Distributed Systems with Justness Rob van Glabbeek	On now Whose dice is it anyway? Session chair: Marie Fortin K. S. Thejaswini











10:00	On now Coffee Break





10:30	On now Express/SOS Workshop Session 1 On the Expressiveness of Asynchronous Processes with Nested Session TypesSjors Wortelboer, Dan Frumin, Jorge A. Pérez The MAY-preorder for timed systems with asynchronous communicationGiovanni Bernardi, Maryline Zhang, Pedro Ribeiro Encoding call-by-push-value in the pi-calculusHans Hüttel, Nikolaj Kristensen, Benjamin Bennetzen, Peter Steffensen Weighted barbed congruenceIwan Quémerais	On now SNR Workshop Session 1 Optimal MDP RepairVenkata Harshavardhan Chinta, Sven Schewe, Qiyi Tang, Shufang Zhu Shielding for Higher-Order SafetyFilip Cano, Thomas A. Henzinger, Konstantin Kueffner Game Semantics for De Morgan AlgebrasCan Baskent, Andrew Lewis-Smith	On now From Individual Interactions to Collective Dynamics — and Back: Why Timing Matters Tatjana Petrov	On now YR-CONCUR Session 1 - Verification Session chair: K. S. Thejaswini Opacity Problems in Timed AutomataSarah Dépernet Designing and Verifying a Post-Quantum Protocol using ProVerifRobert-William Evans, Florian Kammueller Supporting Phased Atomicity in the OpenCL Memory ModelHaining Tong, Keijo Heljanko











11:30			On now Book presentation: Models of Computation based on Automata: Formal Languages and Communicating Processes Jos Baeten





12:00	On now Lunch

















13:30	On now Structural Operational Semantics for String Diagrammatic Languages Fabio Zanasi	On now Active Learning for the Synthesis of POMDP Policies Prince Mathew	On now Abstract Operational Reasoning Henning Urbat	On now YR-CONCUR Session 2 - Games Session chair: Sarvin Bahmani Simple Nash Equilibria for Qualitative Multiplayer GamesMona Alluwaym, Sven Schewe, James C. A. Main Sure-almost-sure and Sure-limit-sure Mean Payoff in Markov Decision ProcessesRaphaël Berthon, Pranshu Gaba, Vaani Goenka, Shibashis Guha, Chandralekha P











14:30	On now Coffee Break





15:00	On now Express/SOS Workshop Session 2 The Theory of Sequential Value PassingEduardo Costa Martins Deadlock-Free Parallel Regions for Projected WorkflowsBenedikt Bollig A Formal Comparison of Controllability Definitions for Deterministic and Nondeterministic AutomataJeroen Keiren, Michel Reniers Discounted-Sum Automata - Reductions between the Universality ProblemsUdi Boker	On now Randomised Decision Making: Expressiveness and Complexity James Main	On now IFIP WG 1.8 Business meeting	On now YR-CONCUR Session 3 - Petri Nets + Logic Forward-Responsibility in Petri NetsCaroline Lemke, Heike Wehrheim Duality for Horn Disjunctive Linear RelationsOm Swostik Mishra, Christoph Haase ATCAL: a model of information manipulation by concurrent announcementsLouwe B. Kuijer, Klara Rawska-Furman











16:00		On now Open Problem Session







16:40

EXPRESS/SOS (Room B)

8:30	On now Registration & Coffee
9:00	On now Expressiveness, Separation and Complexity Results on Multiparty Session Types Nobuko Yoshida
10:00	On now Coffee Break
10:30	On now Express/SOS Workshop Session 1 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
12:00	On now Lunch
13:30	On now Structural Operational Semantics for String Diagrammatic Languages Fabio Zanasi
14:30	On now Coffee Break
15:00	On now Express/SOS Workshop Session 2 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 (Room C)

8:30	On now Registration & Coffee
9:00	On now Can We Change the Game? Reasoning about Dynamic Multi-Agent Systems Munyque Mittelmann
10:00	On now Coffee Break
10:30	On now SNR Workshop Session 1 Optimal MDP Repair Venkata Harshavardhan Chinta, Sven Schewe, Qiyi Tang, Shufang Zhu Shielding for Higher-Order Safety Filip Cano, Thomas A. Henzinger, Konstantin Kueffner Game Semantics for De Morgan Algebras Can Baskent, Andrew Lewis-Smith
12:00	On now Lunch
13:30	On now Active Learning for the Synthesis of POMDP Policies Prince Mathew
14:30	On now Coffee Break
15:00	On now Randomised Decision Making: Expressiveness and Complexity James Main
16:00	On now Open Problem Session

Trends (Room D)

8:30	On now Registration & Coffee
9:00	On now Ensuring Liveness Properties of Distributed Systems with Justness Rob van Glabbeek
10:00	On now Coffee Break
10:30	On now From Individual Interactions to Collective Dynamics — and Back: Why Timing Matters Tatjana Petrov
11:30	On now Book presentation: Models of Computation based on Automata: Formal Languages and Communicating Processes Jos Baeten
12:00	On now Lunch
13:30	On now Abstract Operational Reasoning Henning Urbat
14:30	On now Coffee Break
15:00	On now IFIP WG 1.8 Business meeting

YR-CONCUR (G-FLEX)

8:30	On now Registration & Coffee
9:00	On now Whose dice is it anyway? Session chair: Marie Fortin K. S. Thejaswini
10:00	On now Coffee Break
10:30	On now YR-CONCUR Session 1 - Verification Session chair: K. S. Thejaswini Opacity Problems in Timed Automata Sarah Dépernet Designing and Verifying a Post-Quantum Protocol using ProVerif Robert-William Evans, Florian Kammueller Supporting Phased Atomicity in the OpenCL Memory Model Haining Tong, Keijo Heljanko
12:00	On now Lunch
13:30	On now YR-CONCUR Session 2 - Games Session chair: Sarvin Bahmani Simple Nash Equilibria for Qualitative Multiplayer Games Mona Alluwaym, Sven Schewe, James C. A. Main Sure-almost-sure and Sure-limit-sure Mean Payoff in Markov Decision Processes Raphaël Berthon, Pranshu Gaba, Vaani Goenka, Shibashis Guha, Chandralekha P
14:30	On now Coffee Break
15:00	On now YR-CONCUR Session 3 - Petri Nets + Logic Forward-Responsibility in Petri Nets Caroline Lemke, Heike Wehrheim Duality for Horn Disjunctive Linear Relations Om Swostik Mishra, Christoph Haase ATCAL: a model of information manipulation by concurrent announcements Louwe B. Kuijer, Klara Rawska-Furman

Caption

SNR

Trends

YR-CONCUR