ATVA 2021 Program

Welcome to the 19th International Symposium on Automated Technology for Verification and Analysis(ATVA 2021)!
ATVA 2021 was planned to be hosted on the Gold Coast, Australia, in late October 2021. However, due tothe pandemic and travel restrictions, the Steering Committee decided to host the conference virtually.
ATVA 2021 received 75 submissions covering theory and applications in automated verification andanalysis techniques. Each paper was reviewed by at least three reviewers, and the programme committee
accepted 19 Regular Papers and 4 Tool Papers, leading to a competitive and attractive scientificprogramme.

Keynote Speakers

Sir Tony Hoare

Prof Andrew Yao

Prof Moshe Vardi

Prof Somesh Jha

This edition of ATVA is blessed by the presence of four prestigious keynote speakers. The first keynote will
be given by Sir Tony Hoare, a Turing Award and Kyoto Prize laureate. He will discuss the link between
geometry and programming testing. The second keynote speaker, Prof Andrew Chi-Chih Yao of Tsinghua
University, is also a Turing Award and Kyoto Prize laureate. His expertise is in complexity theory andcryptography, and he will present novel ideas about probabilistic reasoning in machine learning. ProfMoshe Vardi of Rice University is another widely recognised top computer scientist and a Godel Prizewinner. He will talk about linear temporal logic and its applications in analysis and synthesis. Last but notleast, Prof Somesh Jha of the University of Wisconsin will present insightful views of security andtrustworthy machine learning. The four talks cover current hot research topics and many new interesting
research directions.
After the success of the workshops of the previous edition, we decided to co-host the conference withthree workshops in related research areas: Security and reliability of Machine Learning (SRML) 2021,organised by Shiqi Wang, Huan Zhang, Kaidi Xu and Suman Jana; the Workshop on Hyperproperties:
Advances in Theory and Practice (HYPER) 2021, organised by Daniel Fremont and Hazem Torfah; and theWorkshop on Open Problems in Learning and Verification of Neural Networks 2021, organised by Anna
Lukina, Guy Avni, Mirco Giacobbe and Christian Schilling. All three workshops will be hosted virtually on
the 18th of October 2021. We thank all the workshop organisers for their hard work.
ATVA 2021 would not have been successful without the contribution and involvement of the ProgrammeCommittee members and the external reviewers who contributed to the review process (with more than225 reviews) and the selection of the best contributions. This event would not exist if authors andcontributors did not submit their proposals. We address our thanks to every person, reviewer, author,
programme committee member and organizing committee member involved in the success of ATVA 2021.
The EasyChair system was set up for the management of ATVA 2021 supporting submission, review andvolume preparation processes. It proved to be a powerful framework.

Sponsors

Although ATVA 2021 will be hosted virtually, the local host and sponsor Griffith University has provided
tremendous help with registration and online facilities. The other sponsors, Formal Methods Europe,Springer LNCS, and the National University of Singapore, have contributed in different forms to help run
the conference smoothly. Many thanks to all the local organisers and sponsors.
We wish to express our special thanks to the General Chair and steering committee members, particularly
Jing Sun, Farn Wang, Jie-Hong Roland Jiang and Yu-Fang Chen, for their valuable support.

Day 1
18/10/2021

Workshops have their own schedules.
Security and Reliability of Machine Learning (SRML) 2021
Workshop on Hyperproperties: Advances in Theory and Practice (HYPER) 2021
Workshop on Open Problems in Learning and Verification of Neural Networks 2021

Day 2
19/10/2021
N.B. The schedule is in Brisbane time.

10:00 – 10:30

Opening

Session 1 (Chair: Guangdong Bai)
10:30 – 11:00

Edi Muškardin, Bernhard K. Aichernig, Ingo Pill, Martin Tappler andAndrea Pferscher
AALpy: An Active Automata Learning Library

11:00 – 11:30

Jean-Raphaël Gaglione, Daniel Neider, Rajarshi Roy, Ufuk Topcu andZhe Xu
Learning Linear Temporal Properties from Noisy Data: A MaxSATbased Approach

11:30 – 12:00

Sara Mohammadinejad, Jyotirmoy V. Deshmukh and Laura Nenzi
Mining Interpretable Spatio-temporal Logic Properties for SpatiallyDistributed Systems

12:00 – 15:30

Day BreakSession 2 (Chair: Yan Xiao)
15:30 – 16:00

Tobias John, Simon Jantsch, Christel Baier and Sascha Klüppelholz
Determinization and Limit-determinization of Emerson-Lei automata

16:00 – 16:30

Alessandro Cimatti, Alberto Griggio and Enrico Magnago
Automatic discovery of fair paths in infinite-state transition systems

16:30 – 17:00

Orna Kupferman, Nir Lavee and Salomon Sickert
Certifying DFA Bounds for Recognition and Separation

17:00 – 17:30
17:30 – 18:30

Afternoon Break (Announcement)
Keynote: Sir Tony Hoare (Chair: Zhe Hou)
A Geometric Theory for Program TestingDay 3
20/10/2021
N.B. The schedule is in Brisbane time.

Session 3 (Chair: Zhe Hou)
10:30 – 11:00

Lukas Stevens and Tobias Nipkow
A Verified Decision Procedure for Orders in Isabelle/HOL

11:00 – 11:30

Dirk Beyer, Karlheinz Friedberger and Stephan Holzner
PJBDD: A BDD Library for Java and Multi-Threading

11:30 – 12:00

Brae Webb, Mark Utting and Ian Hayes
A Formal Semantics of the GraalVM Intermediate Representation

12:00 – 15: 30

Day BreakSession 4 (Chair: Yun Lin)
15:30 – 16:00

Igor Khmelnitsky, Daniel Neider, Rajarshi Roy, Xuan Xie, BenoîtBarbot, Benedikt Bollig, Alain Finkel, Serge Haddad, Martin Leucker
and Lina Ye
Property-Directed Verification and Robustness Certification ofRecurrent Neural Networks

16:00 – 16:30

Peter Gjøl Jensen, Stefan Schmid, Morten Konggaard Schou, Jiri Srba,
Juan Vanerio and Ingo van Duijn
Faster Pushdown Reachability Analysis with Applications in Network
Verification

16:30 – 17:00

Bernd Finkbeiner, Felix Klein, and Niklas Metzger
Live Synthesis

17:00 – 17:30

Afternoon Break

17:30 – 18:30

Keynote: Prof Andrew Yao (Chair: Jin Song Dong)
Probabilistic Reasoning in Machine Learning

Day 4
21/10/2021
N.B. The schedule is in Brisbane time.

9:00 – 10:00

Keynote: Prof Moshe Vardi (Chair: Jun Sun)
Linear Temporal Logic: From Infinite to Finite Horizon

Session 5 (Chair: Rajeev Gore)
10:30 – 11:00

Christel Baier, Florian Funke, Simon Jantsch, Jakob Piribauer andRobin Ziemek
Probabilistic causes in Markov Chains

11:00 – 11:30

Stefan Pranger, Bettina Könighofer, Lukas Posch and Roderick BloemTEMPEST - Synthesis Tool for Reactive Systems and Shields inProbabilistic Environments

11:30 – 12:00

Zixin Huang, Saikat Dutta and Sasa Misailovic
AQUA: Automated Quantized Inference for Probabilistic Programs

12:00 – 15: 30

Day BreakSession 6 (Chair: Tobias Nipkow)
15:30 – 16:00

This session starts at 16:00.

16:00 – 16:30

Vedad Hadžić, Robert Primas and Roderick Bloem
Proving SIFA Protection of Masked Redundant Circuits

16:30 – 17:00

Norine Coenen, Bernd Finkbeiner, Christopher Hahn, Jana Hofmannand Yannick Schillo
Runtime Enforcement of Hyperproperties

Day 522/10/2021
N.B. The schedule is in Brisbane time.

9:00 – 10:00

Keynote: Prof Somesh Jha (Chair: Vijay Ganesh)
Trustworthy Machine Learning and the Security Mindset

Session 7 (Chair: Jing Sun)
10:30 – 11:00

Dario Guidotti, Luca Pulina and Armando Tacchella
pyNever: a Framework for Learning and Verification of NeuralNetworks

11:00 – 11:30

Siddharth Priya, Xiang Zhou, Yusen Su, Yakir Vizel, Yuyan Bao and Arie
Gurfinkel
Verifying Verified Code11:30 – 12:00

Murad Akhundov, Federico Mora, Nick Feng, Vincent Hui and Marsha
Chechik
Verification by Gambling on Program Slices

12:00 – 15: 30

Day BreakSession 8 (Chair: Zhilin Wu)
15:30 – 16:00

Shaun Azzopardi, Nir Piterman and Gerardo Schneider
Incorporating Monitors in Reactive Synthesis without Paying thePrice

16:00 – 16:30

Guillaume Dupont, Yamine Ait Ameur, Marc Pantel and Neeraj Singh
Event-B Refinement for Continuous Behaviours Approximation

16:30 – 17:00

Bernd Finkbeiner and Noemi Passing
Compositional Synthesis of Modular Systems

Conference Organising Committee
General Co-Chairs
Jin Song Dong, National University of Singapore, Singapore
Jing Sun, University of Auckland, New Zealand
Program Co-Chairs
Zhe Hou, Griffith University, Australia
Vijay Ganesh, University of Waterloo, Canada
Steering Committee
Teruo Higashino, Osaka University, Japan
Jie-Hong Roland Jiang, National Taiwan University, Taiwan
Doron A Peled, Bar Ilan University, Israel
Yu-Fang Chen, Institute of Information Science, Academia Sinica, Taiwan
Ichiro Hasuo, National Institute of Informatics, Japan
Yunja Choi, Kyungpook National University, KoreaAdvisory Committee
Insup Lee, University of Pennsylvania, USAAllen Emerson, The University of Texas at Austin, USAHsu-Chun Yen, National Taiwan University, TaiwanFarn Wang, National Taiwan University, Taiwan
Publicity Co-Chairs
Giles Reger, The University of Manchester, UKMeng Sun, Peking University, China
Workshop Co-Chairs
Guy Katz, Hebrew University of Jerusalem, Israel
Rayna Dimitrova, CISPA Helmholtz Center for Information Security, Germany
Program Committee
Erika Abraham, RWTH Aachen University, Germany
Mohamed Faouzi Atig, Uppsala University, Sweden
Christel Baier, TU Dresden, Germany
Stanley Bak, Stony Brook University, USEzio Bartocci, Vienna University of Technology, Austria
Saddek Bensalem, VERIMAG, FranceArmin Biere, Johannes Kepler University Linz, Austria
Nikolaj Bjorner, Microsoft, USAUdi Boker, Interdisciplinary Center (IDC) Herzliya, Israel
Borzoo Bonakdarpour, Michigan State University, US
Luca Bortolussi, University of Trieste, Italy
Jalil Boudjadar, Aarhus University, Denmark
Martin Brain, University of Oxford, UK
Franck Cassez, ConsenSys & Macquarie University, Australia
Supratik Chakraborty, IIT Bombay, India
Krishnendu Chatterjee, Institute of Science and Technology (IST), UKYu-Fang Chen, Academia Sinica, TaiwanChih-Hong Cheng, DENSO AUTOMOTIVE Deutschland GmbH, Germany
Alessandro Cimatti, Fondazione Bruno Kessler, Italy
Hung Dang Van, Vietnam National University, Vietnam
Tien V. Do, Budapest University of Technology and Economics, Hungary
Alexandre Duret-Lutz, LRDE/EPITA, FranceJavier Esparza, Technical University of Munich, Germany
Bernd Finkbeiner, CISPA Helmholtz Center for Information Security, Germany
Pascal Fontaine, Université de Liège, Belgium
Martin Fränzle, Carl von Ossietzky Universität Oldenburg, Germany
Pierre Ganty, IMDEA Software Institute, Spain
Alberto Griggio, Fondazione Bruno Kessler, Italy
Dimitar Guelev, Bulgarian Academy of Sciences, Bulgaria
Keijo Heljanko, University of Helsinki, Finland
Guy Katz, The Hebrew University of Jerusalem, Israel
Siau-Cheng Khoo, National University of Singapore, Singapore
Xuandong Li, Nanjing University, China
Anthony Widjaja Lin, TU Kaiserslautern, Germany
Alexander Nadel, Intel, Israel
Pham Ngoc Hung, Vietnam National University, Vietnam
Aina Niemetz, Stanford University, USA
Tobias Nipkow, The Technical University of Munich, Germany
Doron Peled, Bar Ilan University, Israel
Mathias Preiner, Stanford University, USA
Markus Rabe, Google, USA
Andrew Reynolds, University of Iowa, USAOlli Saarikivi, Aalto University, Finland
Indranil Saha, Indian Institute of Technology Kanpur, India
Sven Schewe, University of Liverpool, UK
Anne-Kathrin Schmuck, Max-Planck-Institute for Software Systems, Germany
Daniel Selsam, Microsoft Research, USA
Gagandeep Singh, VMWare Research and UIUC, USA
Sadegh Soudjani, Newcastle University, UK
Jun Sun, Singapore Management University, Singapore
Sofiene Tahar, Concordia University, Canada
Michael Tautschnig, Queen Mary University of London, UK
Tachio Terauchi, Waseda University, Japan
Aditya Thakur, University of California, Davis, USA
Cesare Tinelli, University of Iowa, USA
Hoang Truong, Vietname National University, VietnameBow-Yaw Wang, Academia Sinica, Taiwan
Zhilin Wu, Chinese Academy of Sciences, China