Timezone: GMT +2

Program details

Conference Day 1: Wednesday, 21 October, 2020
09:00 – 09:15

(Timezone: GMT +2)

Opening Speech by Conference Chair
Welcome message by Conference Steering Commitee Chair
Programme Summary by PC co-chairs
09:15 – 10:15 Keynote 1: First-Order Timed Runtime Verification using BDDs
Klaus Havelund and Doron Peled

Chair: Oleg Sokolsky

10:15 – 10:30 Break
10:30 – 12:20 Session 1: Synthesis and Monitors

Chair: Hoang Truong Anh

59. Explainable Reactive Synthesis
Tom Baumeister, Bernd Finkbeiner and Hazem Torfah
60. Robust Controller Synthesis for Duration Calculus
Kalyani Dole, Ashutosh Gupta and Shankara Narayanan Krishna
83. Dependency-based Compositional Synthesis
Bernd Finkbeiner and Noemi Passing
18. RTAMT: Online Robustness Monitors from STL (tool paper)
Dejan Ničković and Tomoya Yamaguchi
12:20 – 13:30 Lunch Break
13:30 – 15:30 Session 2: Techniques for Verification, Analysis and Testing

Chair: Bernd Finkbeiner

8. Faster Algorithms for Quantitative Analysis of MCs and MDPs with Small Treewidth
Ali Asadi, Krishnendu Chatterjee, Amir Kafshdar Goharshady, Kiarash Mohammadi, and Andreas Pavlogiannis
22. Robustness Verification for Classifier Ensembles
Dennis Gross, Nils Jansen, Guillermo A. Pérez and Stephan
40. Verification of indefinite-horizon POMDPs
Alexander Bork, Sebastian Junges, Joost-Pieter Katoen and Tim Quatmann
45. Verification of a Generative Separation Kernel
Inzemamul Haque, D. D’Souza, Habeeb P, A. Kundu, and Ganesh Babu
15:30 – 15:45 Break
15:45 – 16:45 Session 3: Techniques for Verification, Analysis and Testing (cont.)

Chair: Zhilin Wu

19. RVX – A Tool for Concolic Testing of Embedded Binaries Targeting RISC-V Platforms (tool paper)
Vladimir Herdt, Daniel Große and Rolf Drechsler
46. Peregrine 2.0: Explaining Correctness of Population Protocols through Stage Graphs (tool paper)
Javier Esparza, Martin Helfrich, Stefan Jaax and Philipp J. Meyer
70. DG: Analysis and Slicing of LLVM Bitcode (tool paper)
Marek Chalupa
Conference Day 2: Thursday, 22 October, 2020
09:00 – 10:00 Keynote 2: Verified Textbook Algorithms
Tobias Nipkow, Manuel Eberl and Maximilian P. L. Haslbeck

Chair: Dang Van Hung

10:00 – 10:15
10:00 – 10:30
10:15 – 12:15
10:30 – 12:30
Session 4: Randomization and Probabilistic Systems

Chair: Sven Schewe

31. Proving Non-Inclusion of Büchi Automata
Yong Li, Andrea Turrini, Xuechao Sun and Lijun Zhang
38. Probabilistic Hyperproperties of Markov Decision Processes
Rayna Dimitrova. Bernd Finkbeiner and Hazem Torfah
90. Minimal Witnesses for Probabilistic Timed Automata
Simon Jantsch, Florian Funke and Christel Baier
56. Probabilistic Hyperproperties with Nondeterminism
Erika Ábrahám, Ezio Bartocci, Borzoo Bonakdarpour and Oyendrila Dobe
12:15 – 13:30
12:30 – 13:30
Lunch Break
13:30 – 15:50 Session 5: Neural Networks and Machine Learning

Chair: Thanh-Tho Quan

13. Verifying Recurrent Neural Networks using Invariant Inference
Yuval Jacoby, and Clark Barrett and Guy Katz
25. NeuralExplorer: State Space Exploration of Closed Loop Control Systems Using Neural Networks
Manish Goyal and Parasara Sridhar Duggirala
65. DeepAbstract: Neural Network Abstraction for Accelerating Verification
Pranav Ashok, Vahid Hashemi, Jan Křetı́nský and Stefanie Mohr
89. Faithful and Effective Reward Schemes for Model-Free Reinforcement Learning of Omega-Regular Objectives
Ernst Moritz Hahn, Mateo Perez. Sven Schewe, Fabio Somenzi, Ashutosh Trivedi and Dominik Wojtczak
27. ReachNN*: A Tool for Reachability Analysis of Neural-Network Controlled Systems (tool paper)
Jiameng Fan, Chao Huang, Xin Chen, Wenchao Li and Qi Zhu
15:50 – 16:05 Break
16:05 – 17:05 Session 6: Logics

Chair: Dang Van Hung

17. Context-Aware Temporal Logic for Probabilistic Systems
Mahmoud Elfar, Yu Wang and Miroslav Pajic
49. Multi-Head Monitoring of Metric Dynamic Logic
Martin Raszyk, David Basin and Dmitriy Traytel
Conference Day 3: Friday, 23 October, 2020
09:00 – 10:00 Keynote 3: Formal verification of Move programs for the Libra blockchain
David Dill

Chair: Oleg Sokolsky

10:00 – 10:15 Break
10:15 – 12:45 Session 7: Model Checking and Decision Procedures

Chair: Doron Peled

47. A Decision Procedure for Path Feasibility of String Manipulating Programs with Integer Data Type
Taolue Chen Matthew Hague, Jinlong He, Denghang Hu, Anthony Widjaja Lin, Philipp Rümmer and Zhilin Wu
52. From Checking to Inference: Actual Causality Computations as Optimization Problems
Amjad Ibrahim and Alexander Pretschner
61. Boosting Sequential Consistency Checking using Saturation
Rachid Zennou, Mohamed Faouzi Atig, Ranadeep Biswas, Ahmed Bouajjani, Constantin Enea and Mohammed Erradi
69. Parallel Graph-Based Stateless Model Checking
Magnus Lång and Konstantinos Sagonas
86. Model Checking Branching Properties on Petri Nets with Transits
Bernd Finkbeiner, Manuel Gieseking, Jesko Hecking-Harbusch and Ernst-Rüdiger Olderog
12:45 – 13:30 Lunch Break
13:30 – 16:00 Session 8: Automata

Chair: Deepak D’Souza

14. Practical “Paritizing” of Emerson-Lei Automata
Florian Renkin. Alexandre Duret-Lutz, and Adrien Pommellet
41. Complexity of Verification and Synthesis of Threshold Automata
A. R. Balasubramanian, Javier Esparza, and Marijana Lazić
58. On (I/O)-aware Good-For-Games Automata
Rachel Faran and Orna Kupferman
63. Urgent Partial Order Reduction for Extended Timed Automata
Kim G. Larsen, Marius Mikučionis, Marco Muñiz and Jiřı́ Srba
92. Eliminating Message Counters in Threshold Automata
Ilina Stoilkovska, Igor Konnov, Josef Widder, and Florian Zuleger
16:00 – 16:15 Closing and Presentation of ATVA 2021

Chair: Vo Dinh Hieu

The pdf file of the final program can be downloaded from here.