Program by Day

I0		CONCUR (Room A)

8:30		Live Registration & Coffee





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











10:00		Live Coffee Break





10:30		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		Live Lunch

















13:30		CONCUR Session 2 - Stochastic Games & MDPs II 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		Live Coffee Break



15:00		CONCUR Session 3 - Behavioural Metrics Session chair: Henning Urbat 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		Live Coffee Break



16:30		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	Live Registration & Coffee
9:00	Live Word Automata with Limited Nondeterminism Session chair: Patrick Totzke Qiyi Tang CONCUR
10:00	Live Coffee Break
10:30	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	Live Lunch
13:30	CONCUR Session 2 - Stochastic Games & MDPs II 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	Live Coffee Break
15:00	CONCUR Session 3 - Behavioural Metrics Session chair: Henning Urbat 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	Live Coffee Break
16:30	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		Live Reception

CONCUR (Room A)

18:00	Live Reception

Caption

Invited

CONCUR

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

8:30	Live Registration & Coffee





9:00	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	Live QEST+FORMATS Opening Q+F
		Live QEST+FORMATS Opening Q+F
9:10		Live Monitoring of Timed and Quantitative Systems Kim G. Larsen Q+F











10:10	Live Coffee Break



10:30	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	Q+F Session 1 - Markov Models under Uncertainty 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	Live Lunch

















13:30	CONCUR Session 7 - Time 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	Live Supporting Older Adults Living Independently Jane Hillston Q+F













14:40	Live Coffee Break



15:00	CONCUR Test of Time Session Session chair: Wan Fokkink A New Type System for Deadlock-Free ProcessesNaoki Kobayashi Strategy LogicNir Piterman	Q+F Session 2 - Parametric Games and Automata 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:10	Live Coffee Break



16:30	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	Q+F Session 3 - Learning and Quantum Systems 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	Live Registration & Coffee
9:00	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	Live Coffee Break
10:30	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	Live Lunch
13:30	CONCUR Session 7 - Time 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	Live Coffee Break
15:00	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	Live Coffee Break
16:30	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	Live Registration & Coffee
9:00	Live QEST+FORMATS Opening Q+F
9:10	Live Monitoring of Timed and Quantitative Systems Kim G. Larsen Q+F
10:10	Live Coffee Break
10:30	Q+F Session 1 - Markov Models under Uncertainty 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	Live Lunch
13:30	Live Supporting Older Adults Living Independently Jane Hillston Q+F
14:40	Live Coffee Break
15:00	Q+F Session 2 - Parametric Games and Automata 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:10	Live Coffee Break
16:30	Q+F Session 3 - Learning and Quantum Systems 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	Live Registration & Coffee





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











10:00	Live Coffee Break





10:30	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	Q+F Session 4 - Stochastic Model Checking 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	FMICS Session 1 - Formal Verification 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	Live Lunch

















13:30	CONCUR Session 10 - Parameterised Verification 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	Q+F Session 5 - Probabilistic and Temporal Logic Semantics 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	Live Application of Formal Methods to Design and Verification of Autonomous Space Systems Julia Badger FMICS













14:40	Live Coffee Break



15:00	Live An Introduction to Multi-Environment Markov Decision Processes Session chair: Patrick Totzke Jean-François Raskin CONCUR	Q+F Session 6 - Continuous and Hybrid Systems 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	FMICS Session 2 - Advanced Reasoning 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:10

CONCUR (Room A)

8:30	Live Registration & Coffee
9:00	Live Reasoning About Probabilistic Loops, Moment by Moment Session chair: Max Tschaikowski Ezio Bartocci Joint Room A
10:00	Live Coffee Break
10:30	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	Live Lunch
13:30	CONCUR Session 10 - Parameterised Verification 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	Live Coffee Break
15:00	Live An Introduction to Multi-Environment Markov Decision Processes Session chair: Patrick Totzke Jean-François Raskin CONCUR

QEST+FORMATS (Room B)

8:30	Live Registration & Coffee
9:00	Live Reasoning About Probabilistic Loops, Moment by Moment Session chair: Max Tschaikowski Ezio Bartocci Joint Room A
10:00	Live Coffee Break
10:30	Q+F Session 4 - Stochastic Model Checking 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	Live Lunch
13:30	Q+F Session 5 - Probabilistic and Temporal Logic Semantics 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:40	Live Coffee Break
15:00	Q+F Session 6 - Continuous and Hybrid Systems 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	Live Registration & Coffee
9:00	Live Reasoning About Probabilistic Loops, Moment by Moment Session chair: Max Tschaikowski Ezio Bartocci Joint Room A
10:00	Live Coffee Break
10:30	FMICS Session 1 - Formal Verification 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	Live Lunch
13:30	Live Application of Formal Methods to Design and Verification of Autonomous Space Systems Julia Badger FMICS
14:40	Live Coffee Break
15:00	FMICS Session 2 - Advanced Reasoning 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		Live Boat Tour / Dinner (Boarding at 7:15pm)

CONCUR (Room A)

19:00	Live Boat Tour / Dinner (Boarding at 7:15pm)

QEST+FORMATS (Room B)

19:00	Live Boat Tour / Dinner (Boarding at 7:15pm)

FMICS (Room D)

19:00	Live Boat Tour / Dinner (Boarding at 7:15pm)

Caption

Invited

CONCUR

Q+F

FMICS

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

8:30	Live Registration & Coffee





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











10:00	Live Coffee Break





10:30	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	Q+F Session 7 - Dependability and Security Analysis 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	FMICS Session 3 - Advanced Analysis 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	Live Lunch

















13:30	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	Q+F Session 8 - Queueing and Performance Models 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	Live Reducing Time to Market through Formal Methods Colin O'Halloran FMICS













14:40	Live Coffee Break



15:00	Live On the role of prose in specifications Session chair: Ana Sokolova Jade Alglave CONCUR	Q+F Session 9 - Timed Automata and Languages 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	Live Panel Session discussing the Industrial use of Formal Methods













16:10	Live Coffee Break



16:30	CONCUR Session 13 - Partial Observation 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	Q+F Session 10 - Verification Tools 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:40

CONCUR (Room A)

8:30	Live Registration & Coffee
9:00	Live Category Theory for Fast Model Checking Algorithms Session chair: Ana Sokolova Ichiro Hasuo Joint Room A
10:00	Live Coffee Break
10:30	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	Live Lunch
13:30	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	Live Coffee Break
15:00	Live On the role of prose in specifications Session chair: Ana Sokolova Jade Alglave CONCUR
16:10	Live Coffee Break
16:30	CONCUR Session 13 - Partial Observation 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

QEST+FORMATS (Room B)

8:30	Live Registration & Coffee
9:00	Live Category Theory for Fast Model Checking Algorithms Session chair: Ana Sokolova Ichiro Hasuo Joint Room A
10:00	Live Coffee Break
10:30	Q+F Session 7 - Dependability and Security Analysis 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	Live Lunch
13:30	Q+F Session 8 - Queueing and Performance Models 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:40	Live Coffee Break
15:00	Q+F Session 9 - Timed Automata and Languages 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:10	Live Coffee Break
16:30	Q+F Session 10 - Verification Tools 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	Live Registration & Coffee
9:00	Live Category Theory for Fast Model Checking Algorithms Session chair: Ana Sokolova Ichiro Hasuo Joint Room A
10:00	Live Coffee Break
10:30	FMICS Session 3 - Advanced Analysis 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	Live Lunch
13:30	Live Reducing Time to Market through Formal Methods Colin O'Halloran FMICS
14:40	Live Coffee Break
15:00	Live Panel Session discussing the Industrial use of Formal Methods
16:10	Live Coffee Break

18:00		Live Football

CONCUR (Room A)

18:00	Live Football

QEST+FORMATS (Room B)

18:00	Live Football

FMICS (Room D)

18:00	Live Football

Caption

Invited

CONCUR

Q+F

FMICS

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

8:30	Live Registration & Coffee





9:00	Live Expressiveness, Separation and Complexity Results on Multiparty Session Types Nobuko Yoshida	Live SNR Workshop Session 1	Live Ensuring Liveness Properties of Distributed Systems with Justness Rob van Glabbeek Trends	Live YR-CONCUR Workshop Session 1











10:00	Live Coffee Break





10:30	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	Live SNR Workshop Session 2	Live TBD Tatjana Petrov Trends	Live YR-CONCUR Workshop Session 2











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





12:00	Live Lunch

















13:30	Live Structural Operational Semantics for String Diagrammatic Languages Fabio Zanasi	Live SNR Workshop Session 3	Live Abstract Operational Reasoning Henning Urbat Trends	Live YR-CONCUR Workshop Session 3











14:30	Live Coffee Break





15:00	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	Live SNR Workshop Session 4	Live IFIP WG 1.8 Business meeting	Live YR-CONCUR Workshop Session 4



















16:40

EXPRESS/SOS (Room B)

8:30	Live Registration & Coffee
9:00	Live Expressiveness, Separation and Complexity Results on Multiparty Session Types Nobuko Yoshida
10:00	Live Coffee Break
10:30	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	Live Lunch
13:30	Live Structural Operational Semantics for String Diagrammatic Languages Fabio Zanasi
14:30	Live Coffee Break
15:00	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	Live Registration & Coffee
9:00	Live SNR Workshop Session 1
10:00	Live Coffee Break
10:30	Live SNR Workshop Session 2
12:00	Live Lunch
13:30	Live SNR Workshop Session 3
14:30	Live Coffee Break
15:00	Live SNR Workshop Session 4

Trends (Room D)

8:30	Live Registration & Coffee
9:00	Live Ensuring Liveness Properties of Distributed Systems with Justness Rob van Glabbeek Trends
10:00	Live Coffee Break
10:30	Live TBD Tatjana Petrov Trends
11:30	Live Book presentation: Models of Computation based on Automata: Formal Languages and Communicating Processes Jos Baeten Trends
12:00	Live Lunch
13:30	Live Abstract Operational Reasoning Henning Urbat Trends
14:30	Live Coffee Break
15:00	Live IFIP WG 1.8 Business meeting

YR-CONCUR (G-FLEX)

8:30	Live Registration & Coffee
9:00	Live YR-CONCUR Workshop Session 1
10:00	Live Coffee Break
10:30	Live YR-CONCUR Workshop Session 2
12:00	Live Lunch
13:30	Live YR-CONCUR Workshop Session 3
14:30	Live Coffee Break
15:00	Live YR-CONCUR Workshop Session 4

Caption

Invited

SNR

Trends

YR-CONCUR