Table of Contents

• Front Matter, Table of Contents, Preface, Conference Organization [doi]
• Deciding What Is Good-For-MDPsSven Schewe, Qiyi Tang 0001, Tansholpan Zhanabekova. [doi]
• Constraint Automata on Infinite Data Trees: from CTL(ℤ)/ CTL^*}(ℤ) to Decision ProceduresStéphane Demri, Karin Quaas. [doi]
• Games with Trading of ControlOrna Kupferman, Noam Shenwald. [doi]
• Model-Checking Parametric Lock-Sharing Systems Against Regular ConstraintsCorto Mascle, Anca Muscholl, Igor Walukiewicz. [doi]
• On Verifying Concurrent Programs Under Weakly Consistent Models (Invited Talk)Ahmed Bouajjani. [doi]
• History-Deterministic Parikh AutomataEnzo Erlich, Shibashis Guha, Ismaël Jecker, Karoliina Lehtinen, Martin Zimmermann 0002. [doi]
• Expressiveness Results for an Inductive Logic of Separated RelationsRadu Iosif, Florian Zuleger. [doi]
• Universal Quantification Makes Automatic Structures Hard to DecideChristoph Haase, Radoslaw Piórkowski. [doi]
• Faithful Simulation of Randomized BFT Protocols on Block DAGsHagit Attiya, Constantin Enea, Shafik Nassar. [doi]
• History-Deterministic Vector Addition SystemsSougata Bose, David Purser, Patrick Totzke. [doi]
• Real Equation Systems with Alternating Fixed-PointsJan Friso Groote, Tim A. C. Willemse. [doi]
• A Game of PawnsGuy Avni, Pranav Ghorpade, Shibashis Guha. [doi]
• The Best of Both Worlds: Model-Driven Engineering Meets Model-Based TestingP. H. M. van Spaendonck, Tim A. C. Willemse. [doi]
• Geometry of Reachability Sets of Vector Addition SystemsRoland Guttenberg, Mikhail A. Raskin, Javier Esparza. [doi]
• Contextual Behavioural MetricsUgo Dal Lago, Maurizio Murgia 0001. [doi]
• Hypernode AutomataEzio Bartocci, Thomas A. Henzinger, Dejan Nickovic, Ana Oliveira da Costa. [doi]
• Safety Analysis of Parameterised Networks with Non-Blocking Rendez-VousLucie Guillou, Arnaud Sangnier, Nathalie Sznajder. [doi]
• Visibility and Separability for a Declarative Linearizability Proof of the Timestamped StackJesús Domínguez, Aleksandar Nanevski. [doi]
• CONCUR Test-Of-Time Award 2023 (Invited Paper)Bengt Jonsson 0001, Marta Kwiatkowska, Igor Walukiewicz. [doi]
• About Decisiveness of Dynamic Probabilistic ModelsAlain Finkel, Serge Haddad, Lina Ye. [doi]
• Computing Minimal Distinguishing Hennessy-Milner Formulas is NP-Hard, but Variants are TractableJan Martens 0001, Jan Friso Groote. [doi]
• DNN Verification, Reachability, and the Exponential Function ProblemOmri Isac, Yoni Zohar, Clark W. Barrett, Guy Katz. [doi]
• Complexity of Membership and Non-Emptiness Problems in Unbounded Memory AutomataClément Bertrand, Cinzia Di Giusto, Hanna Klaudel, Damien Regnault. [doi]
• Subtyping Context-Free Session TypesGil Silva 0002, Andreia Mordido, Vasco T. Vasconcelos. [doi]
• Process-Algebraic Models of Multi-Writer Multi-Reader Non-Atomic RegistersMyrthe S. C. Spronck, Bas Luttik. [doi]
• Compositional Correctness and Completeness for Symbolic Partial Order ReductionÅsmund Aqissiaq Arild Kløvstad, Eduard Kamburjan, Einar Broch Johnsen. [doi]
• The Semilinear Home-Space Problem Is Ackermann-Complete for Petri NetsPetr Jancar, Jérôme Leroux. [doi]
• Safety and Liveness of Quantitative AutomataUdi Boker, Thomas A. Henzinger, Nicolas Mazzocchi, N. Ege Saraç. [doi]
• A General Approach to Under-Approximate Reasoning About Concurrent ProgramsAzalea Raad, Julien Vanegue, Josh Berdine, Peter W. O'Hearn. [doi]
• Quantitative Verification with Neural NetworksAlessandro Abate, Alec Edwards, Mirco Giacobbe, Hashan Punchihewa, Diptarko Roy. [doi]
• Reachability and Bounded Emptiness Problems of Constraint Automata with Prefix, Suffix and InfixJakub Michaliszyn, Jan Otop, Piotr Wieczorek. [doi]
• Priority Downward ClosuresAshwani Anand, Georg Zetzsche. [doi]
• Separability and Non-Determinizability of WSTSEren Keskin, Roland Meyer 0001. [doi]
• Modal Logics for Mobile Processes RevisitedTiange Liu, Alwen Tiu, Jim de Groot. [doi]
• Asymptotic Complexity Estimates for Probabilistic Programs and Their VASS AbstractionsMichal Ajdarów, Antonín Kucera 0001. [doi]
• Monus Semantics in Vector Addition Systems with StatesPascal Baumann 0001, Khushraj Madnani, Filip Mazowiecki, Georg Zetzsche. [doi]
• Satisfiability Checking of Multi-Variable TPTL with Unilateral Intervals Is PSPACE-CompleteShankara Narayanan Krishna, Khushraj Nanik Madnani, Rupak Majumdar, Paritosh K. Pandya. [doi]
• Singly Exponential Translation of Alternating Weak Büchi Automata to Unambiguous Büchi AutomataYong Li 0031, Sven Schewe, Moshe Y. Vardi. [doi]
• Probabilistic Operational CorrespondenceAnna Schmitt 0002, Kirstin Peters. [doi]