Zoom Meeting No: 551 491 1489, Passcode: 202210
October 25th, 2022.
| Time | Speaker | Chair | Tutorial |
|---|---|---|---|
| Beijing 13:00-14:30 Paris 07:00-08:30 San Francisco 22:00-23:30 |
Constantin Enea, LIX, Ecole Polytechnique, France |
Xinyu Feng | Verifying Consistency of Large-Scale Storage Systems and Applications [Video] |
| Beijing 14:30-14:45 Paris 08:30-08:45 San Francisco 23:30-23:45 |
Break | ||
| Beijing 14:45-16:15 Paris 08:45-10:15 San Francisco 23:45-01:15 |
Constantin Enea, LIX, Ecole Polytechnique, France |
Xinyu Feng | Verifying Consistency of Large-Scale Storage Systems and Applications |
| Beijing 22:00-23:30 Paris 16:00-17:30 San Francisco 07:00-08:30 |
Mahesh Viswanathan, University of Illinois Urbana-Champaign, USA |
Lijun Zhang | Verifying the Privacy and Accuracy of Algorithms for Differential Privacy [Video] |
| Beijing 23:30-23:45 Paris 17:30-17:45 San Francisco 08:30-08:45 |
Break | ||
| Beijing 23:45-01:15 Paris 17:45-19:15 San Francisco 08:45-10:15 |
Mahesh Viswanathan, University of Illinois Urbana-Champaign, USA |
Lijun Zhang | Verifying the Privacy and Accuracy of Algorithms for Differential Privacy |
October 26th, 2022.
| Time | Session | Talks |
|---|---|---|
| Beijing 13:00-13:15 Paris 07:00-07:15 San Francisco 22:00-22:15 |
Opening | |
| Beijing 13:15-14:15 Paris 07:15-08:15 San Francisco 22:15-23:15 |
Keynote I (Chair: Lijun Zhang) |
Sanjit A. Seshia, Runtime Assurance for Verified AI-Based Autonomy [Video] |
| Beijing 14:15-15:30 Paris 08:15-09:30 San Francisco 23:15-00:30 |
Reinforcement Learning (Chair: Jun Sun) |
14:15-14:40 Masaki Waga, Ezequiel Castellano, Sasinee Pruekprasert, Stefan Klikovits, Toru Takisaka and Ichiro Hasuo, Dynamic Shielding for Reinforcement Learning in Black-Box Environments [Video]
14:40-15:05 Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi and Dominik Wojtczak, An Impossibility Result in Automata-Theoretic Reinforcement Learning [Video] 15:05-15:30 Julius Adelt, Daniel Brettschneider and Paula Herber, Reusable Contracts for Safe Integration of Reinforcement Learning in Hybrid Systems [Video] |
| Beijing 15:30-15:45 Paris 09:30-09:45 San Francisco 00:30-00:45 |
Break | |
| Beijing 15:45-17:15 Paris 09:45-11:15 San Francisco 00:45-02:15 |
Program analysis and verification (Chair: Taolue Chen) |
15:45-16:00 Sören Tempel, Vladimir Herdt and Rolf Drechsler, SISL: Concolic Testing of Structured Binary Input Formats via Partial Specification [Video]
16:00-16:25 Sanjana Singh, Divyanjali Sharma, Ishita Jaju and Subodh Sharma, Fence Synthesis for the C11 Memory Model [Video] 16:25-16:50 Anand Yeolekar, Ravindra Metta, Clara Hobbs and Samarjit Chakraborty, Checking Scheduling-induced Violations of Control Safety Properties [Video] 16:50-17:15 Hannes Kallwies, Martin Leucker and Cesar Sanchez, Symbolic Runtime Verification for Monitoring under Uncertainties and Assumptions [Video] |
| Beijing 22:00-22:10 Paris 16:00-16:10 San Francisco 07:00-07:10 |
Advertisement for ATVA 2023 | |
| Beijing 22:10-23:10 Paris 16:10-17:10 San Francisco 07:10-08:10 |
Keynote II (Chair: Naijun Zhan) |
Xinyu Feng, Compositional Reasoning about Concurrent Randomized Programs [Video] |
| Beijing 23:10-00:25 Paris 17:10-18:25 San Francisco 08:10-09:25 |
SMT and verification (Chair: Philipp Rummer) |
23:10-23:35 Alessandro Cimatti, Alberto Griggio, Enrico Lipparini and Roberto Sebastiani, Handling Polynomial and Transcendental Functions in SMT via Unconstrained Optimisation and Topological Degree Test [Video]
23:35-00:00 Alessandro Cimatti, Alberto Griggio and Gianluca Redondi, Verification of SMT Systems with Quantifiers [Video] 00:00-00:25 Jiong Yang, Supratik Chakraborty and Kuldeep S. Meel, Projected Model Counting: Beyond Independent Support [Video] |
October 27th, 2022.
| Time | Session | Talks |
|---|---|---|
| Beijing 13:00-14:00 Paris 07:00-08:00 San Francisco 22:00-23:00 |
Keynote III (Chair: Ahmed Bouajjani) |
Shaz Qadeer, The Civl Verifier [Video] |
| Beijing 14:00-15:05 Paris 08:00-09:05 San Francisco 23:00-00:05 |
Automata and Applications (Chair: Zhilin Wu) |
14:00-14:25 Bader Abu Radi and Orna Kupferman, Minimization of Automata for Liveness Languages [Video]
14:25-14:50 Norine Coenen, Bernd Finkbeiner, Hadar Frenkel, Christopher Hahn, Niklas Metzger and Julian Siber, Temporal Causality in Reactive Systems [Video] 14:50-15:05 Peter Gjøl Jensen, Stefan Schmid, Morten Konggaard Schou and Jiri Srba, PDAAAL: A Library for Reachability Analysis of Weighted Pushdown Systems [Video] |
| Beijing 15:05-15:20 Paris 09:05-09:20 San Francisco 00:05-00:20 |
Break | |
| Beijing 15:20-16:35 Paris 09:20-10:35 San Francisco 00:20-01:35 |
Active learning (Chair: Yu-Fang Chen) |
15:20-15:45 Xiaochen Tang, Wei Shen, Miaomiao Zhang, Jie An, Bohua Zhan and Naijun Zhan, Learning Deterministic One-Clock Timed Automata via Mutation Testing [Video]
15:45-16:10 Runqing Xu, Jie An and Bohua Zhan, Active Learning of One-Clock Timed Automata using Constraint Solving [Video] 16:10-16:35 Dana Fisman and Sagi Saadon, Learning and Characterizing Fully-Ordered Lattice Automata [Video] |
| Beijing 22:00-23:00 Paris 16:00-17:00 San Francisco 07:00-08:00 |
Keynote IV (Chair: Orna Kupferman) |
Jean-Francois Raskin, Subgame Perfect Equilibrium with an Algorithmic Perspective [Video] |
| Beijing 23:00-00:20 Paris 17:00-18:20 San Francisco 08:00-09:20 |
Probabilistic and stochastic systems (Chair: David Jansen) |
23:00-23:25 Muqsit Azeem, Alexandros Evangelidis, Jan Kretinsky, Alexander Slivinskiy and Maximilian Weininger, Optimistic and Topological Value Iteration for Simple Stochastic Games [Video]
23:25-23:50 Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi and Dominik Wojtczak, Alternating Good-for-MDPs Automata [Video] 23:50-00:05 Tobias Meggendorfer, PET – Partial Exploration Tool for Probabilistic Verification [Video] 00:05-00:20 Martijn Goorden, Peter Gjøl Jensen, Kim Guldstrand Larsen, Mihhail Samusev, Jiri Srba and Guohan Zhao, STOMPC: Stochastic Model-Predictive Control with Uppaal Stratego [Video] |
October 28th, 2022.
| Time | Session | Talks |
|---|---|---|
| Beijing 13:00-14:00 Paris 07:00-08:00 San Francisco 22:00-23:00 |
Keynote V (Chair: Lukas Holik) |
Mohamed Faouzi Atig, Flattening String Constraints [Video] |
| Beijing 14:00-15:15 Paris 08:00-09:15 San Francisco 23:00-00:15 |
Synthesis and repair (Chair: Fei He) |
14:00-14:25 Miriam García Soto, Thomas Henzinger and Christian Schilling, Synthesis of Parametric Hybrid Automata from Time Series [Video]
14:25-14:50 Vrunda Dave, Krishna S, Vishnu Murali and Ashutosh Trivedi, Optimal Repair For Omega-regular Properties [Video] 14:50-15:15 Reiya Noguchi, Ocan Sankur, Thierry Jéron, Nicolas Markey and David Mentré, Repairing Real-Time Requirements [Video] |
| Beijing 15:15-15:30 Paris 09:15-09:30 San Francisco 00:15-00:30 |
Break | |
| Beijing 15:30-16:35 Paris 09:30-10:35 San Francisco 00:30-01:35 |
Verification of neural networks (Chair: Youcheng Sun) |
15:30-15:45 Matan Ostrovsky, Clark Barrett and Guy Katz, An Abstraction-Refinement Approach to Verifying Convolutional Neural Networks [Video]
15:45-16:10 Chih-Hong Cheng, Changshun Wu, Emmanouil Seferis and Saddek Bensalem, Prioritizing Corners in OoD Detectors via Symbolic String Manipulation [Video] 16:10-16:35 Chao Huang, Jiameng Fan, Xin Chen, Wenchao Li and Qi Zhu, POLAR: A Polynomial Arithmetic Framework for Verifying Neural-Network Controlled Systems [Video] |
| Beijing 16:35-16:45 Paris 10:35-10:45 San Francisco 01:35-01:45 |
Closing: Announcement of Best Paper Award | |