Tuesday 19/09 | Wednesday 20/09 | Thursday 21/09 | Friday 22/09 | |
---|---|---|---|---|
09:00-10:00 | Neural networks | Inv. talk: Joost-Pieter Katoen | Inv. talk: Jaco van de Pol | Inv. talk: Ahmed Bouajjani |
10:00-10:20 | Coffee break | |||
10:20-12:20 | Automata I | Verification | Computational models | Verification and testing |
12:20-13:45 | Lunch / S.C. meeting | Test-of-time award talk; Lunch | Lunch | |
13:45-15:45 | 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 |
15:45-16:00 | Coffee break | Coffee break | ||
16:00-17:30 | Games and equation systems | Inv. talk: D. Parker; TPTL | Logic | |
17:30-18:00 | Soccer match | | ||
18:00-20:00 | Conference dinner |
Tuesday
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
Wednesday
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
Thursday
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.
Friday
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