Tuesday 19/09
Wednesday 20/09
Thursday 21/09
Friday 22/09
Neural networks
Inv. talk: Joost-Pieter Katoen
Inv. talk: Jaco van de Pol
Inv. talk: Ahmed Bouajjani
Coffee break
Automata I
Computational models
Verification and testing
Lunch / S.C. meeting
Test-of-time award talk; Lunch
Well-structured transition systems / Inv. talk: N. Markey @ FORMATS
Boat trip on Scheldt river
Automata II / Inv. talk: A. Slobodova @ FMICS
Concurrency models / Inv. talk: F. Oliehoek @ QEST
Coffee break
Coffee break
Games and equation systems
Inv. talk: D. Parker; TPTL

Soccer match


Conference dinner


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


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


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


Chair: Patrick Totzke