Programme

Neural networks

Chair: Guillermo A. Perez

• Omri Isac, Yoni Zohar, Clark Barrett and Guy Katz. DNN Verification, Reachability, and the Exponential Function Problem 
• Alessandro Abate, Alec Edwards, Mirco Giacobbe, Hashan Punchihewa and Diptarko Roy. Quantitative Verification With Neural Networks
  

Automata I

Chair: Jean-Francois Raskin

• ​Clément Bertrand, Cinzia Di Giusto, Hanna Klaudel and Damien Regnault. Complexity of Membership and Non-Emptiness Problems in Unbounded Memory Automata
• Ezio Bartocci, Thomas Henzinger, Dejan Nickovic and Ana Oliveira Da Costa. Hypernode Automata
• Udi Boker, Thomas A. Henzinger, Nicolas Mazzocchi and N. Ege Saraç. Safety and Liveness of Quantitative Automata
• Stephane Demri and Karin Quaas. Constraint Automata on Infinite Data Trees: From CTL(Z)/CTL*(Z) To Decision Procedures
  

Invited talk: Nicolas Markey

Computing the Price of Anarchy in Atomic Network Congestion Games

Well-structured transition systems

Chair: Filip Mazowiecki

• ​Pascal Baumann, Khushraj Madnani, Filip Mazowiecki and Georg Zetzsche. Monus semantics in vector addition systems with states
• [Best Paper] Eren Keskin and Roland Meyer. Separability and Non-Determinizability of WSTS
• Petr Jancar and Jérôme Leroux. Semilinear Home-Space Problem is Ackermann-Complete for Petri Nets
• Roland Guttenberg, Mikhail Raskin and Javier Esparza. Geometry of Reachability Sets of Vector Addition Systems
  

Games and equation systems

Chair: Jerome Leroux

• ​Jan Friso Groote and Tim A.C. Willemse. Real Equation Systems with Alternating Fixed-points
• Guy Avni, Pranav Ghorpade and Shibashis Guha. A Game of Pawns
• Noam Shenwald and Orna Kupferman. Games with Trading of Control
  

Invited talk: Joost-Pieter Katoen

Chair: Alessandro Cimatti

Verification Conquers Fault Tree Analysis

Verification

Chair: Pedro D'Argenio

• ​Jesús Héctor Domínguez Sánchez and Aleksandar Nanevski. Visibility and Separability for a Declarative Linearizability Proof of the Timestamped Stack
• Anna Schmitt and Kirstin Peters. Probabilistic Operational Correspondence
• Anca Muscholl, Corto Mascle and Igor Walukiewicz. Model-checking parametric lock-sharing systems against regular constraints
• Lucie Guillou, Arnaud Sangnier and Nathalie Sznajder. Safety Analysis of Parameterised Networks with Non-Blocking Rendez-Vous
  

Test-of-time award

Chair: Javier Esparza

• ​Jean Krivine. Reversible Communicating Systems
  

Invited talk: Jaco van de Pol

Chair: Wan Fokkink

Encoding Planning and Games in SAT and QBF

Computational models

Chair: Arnaud Sangnier

• ​Sven Schewe, Qiyi Tang and Tansholpan Zhanabekova. Deciding What is Good-for-MDPs
• Alain Finkel, Serge Haddad and Lina Ye. About Decisiveness of Dynamic Probabilistic Models
• Ashwani Anand and Georg Zetzsche. Priority downward closures
• Michal Ajdarow and Antonin Kucera. Asymptotic Complexity Estimates for Probabilistic Programs and their VASS Abstractions
  

Automata II

Chair: Guillermo A. Perez

• ​Sougata Bose, David Purser and Patrick Totzke. History-deterministic Vector Addition Systems
  
• Enzo Erlich, Shibashis Guha, Ismaël Jecker, Karoliina Lehtinen and Martin Zimmermann. History-deterministic Parikh Automata
  
• Jakub Michaliszyn, Jan Otop and Piotr Wieczorek. Reachability and Bounded Emptiness Problems of Constraint Automata with Prefix, Suffix and Infix
• Yong Li, Sven Schewe and Moshe Vardi. Singly Exponential Translation of Alternating Weak Buchi Automata to Unambiguous Buchi Automata

Invited talk: Dave Parker

Multi-Agent Verification and Control with Probabilistic Model Checking

TPTL

Chair: Jeremy Sproston

• ​Krishna S, Khushraj Madnani, Rupak Majumdar and Paritosh Pandya. Satisfiability Checking For Multi-clock Unilateral TPTL is PSPACE Complete.
  

Invited talk: Ahmed Bouajjani

Chair: Igor Walukiewicz

On the verification of concurrent programs under weak consistency models

Verification and testing

Chair: Guillermo A. Perez

• ​Hagit Attiya, Constantin Enea and Shafik Nassar. Faithful Simulation of Randomized BFT Protocols on Block DAGs
• Åsmund Aqissiaq Arild Kløvstad, Eduard Kamburjan and Einar Broch Johnsen. Compositional Correctness and Completeness for Symbolic Partial Order Reduction
• Azalea Raad, Julien Vanegue, Josh Berdine and Peter O'Hearn. A General Approach to Under-approximate Reasoning about Concurrent Programs
• Flip Van Spaendonck and Tim Willemse. The Best of Both Worlds: Model-Driven Engineering meets Model-Based Testing
  

Concurrency models

Chair: Jean-Francois Raskin

• ​Myrthe Spronck and Bas Luttik. Process-Algebraic Models of Multi-Writer Multi-Reader Non-Atomic Registers
• Gil Silva, Andreia Mordido and Vasco Vasconcelos. Subtyping Context-Free Session Types
• Jan Martens and Jan Friso Groote. Computing minimal distinguishing Hennessy-Milner formulas is NP-hard, but variants are tractable
• Ugo Dal Lago and Maurizio Murgia. Contextual Behavioural Metrics
  

Logic

Chair: Patrick Totzke

• ​Tiange Liu, Alwen Tiu and Jim de Groot. Modal logics for mobile processes revisited
• Christoph Haase and Radosław Piórkowski. Universal quantification makes automatic structures hard to decide
• [Online] Radu Iosif and Florian Zuleger. Expressiveness Results for an Inductive Logic of Separated Relations​