{"id":34,"date":"2017-12-15T22:02:50","date_gmt":"2017-12-15T22:02:50","guid":{"rendered":"http:\/\/atva-conference.org\/?page_id=34"},"modified":"2022-11-02T16:19:38","modified_gmt":"2022-11-02T16:19:38","slug":"program","status":"publish","type":"page","link":"https:\/\/atva-conference.org\/2022\/program\/","title":{"rendered":"Program"},"content":{"rendered":"

Zoom Meeting No: 551 491 1489, Passcode: 202210<\/p>\n

October 25th<\/sup>, 2022.<\/h1>\n\n\n\n\n\n<\/colgroup>\n\n\n\n\n\n\n\n\n\n\n
Time<\/th>\nSpeaker<\/th>\nChair<\/th>\nTutorial<\/th>\n<\/tr>\n<\/thead>\n
Beijing 13:00-14:30
\nParis 07:00-08:30
\nSan Francisco 22:00-23:30<\/td>\n		Constantin Enea,
\nLIX, Ecole Polytechnique, France<\/td>\n		Xinyu Feng<\/td>\nVerifying Consistency of Large-Scale Storage Systems and Applications<\/a>
\n[Video<\/a>]<\/span><\/td>\n<\/tr>\n
Beijing 14:30-14:45
\nParis 08:30-08:45
\nSan Francisco 23:30-23:45<\/td>\n		Break<\/td>\n<\/tr>\n
Beijing 14:45-16:15
\nParis 08:45-10:15
\nSan Francisco 23:45-01:15<\/td>\n		Constantin Enea,
\nLIX, Ecole Polytechnique, France<\/td>\n		Xinyu Feng<\/td>\nVerifying Consistency of Large-Scale Storage Systems and Applications<\/a><\/td>\n<\/tr>\n
<\/td>\n<\/td>\n<\/td>\n<\/td>\n<\/tr>\n
Beijing 22:00-23:30
\nParis 16:00-17:30
\nSan Francisco 07:00-08:30<\/td>\n		Mahesh Viswanathan,
\nUniversity of Illinois Urbana-Champaign, USA<\/td>\n		Lijun Zhang<\/td>\nVerifying the Privacy and Accuracy of Algorithms for Differential Privacy<\/a>
\n[Video<\/a>]<\/span><\/td>\n<\/tr>\n
Beijing 23:30-23:45
\nParis 17:30-17:45
\nSan Francisco 08:30-08:45<\/td>\n		Break<\/td>\n<\/tr>\n
Beijing 23:45-01:15
\nParis 17:45-19:15
\nSan Francisco 08:45-10:15<\/td>\n		Mahesh Viswanathan,
\nUniversity of Illinois Urbana-Champaign, USA<\/td>\n		Lijun Zhang<\/td>\nVerifying the Privacy and Accuracy of Algorithms for Differential Privacy<\/a><\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n

October 26th<\/sup>, 2022.<\/h1>\n\n\n\n\n<\/colgroup>\n\n\n\n\n\n\n\n\n\n\n\n\n
Time<\/th>\nSession<\/th>\nTalks<\/th>\n<\/tr>\n<\/thead>\n
Beijing 13:00-13:15
\nParis 07:00-07:15
\nSan Francisco 22:00-22:15<\/td>\n		Opening<\/td>\n<\/tr>\n
Beijing 13:15-14:15
\nParis 07:15-08:15
\nSan Francisco 22:15-23:15<\/td>\n		Keynote I
\n(Chair: Lijun Zhang)<\/td>\n		Sanjit A. Seshia,
\nRuntime Assurance for Verified AI-Based Autonomy<\/a>
\n[Video<\/a>]<\/span><\/td>\n<\/tr>\n
Beijing 14:15-15:30
\nParis 08:15-09:30
\nSan Francisco 23:15-00:30<\/td>\n		Reinforcement Learning
\n(Chair: Jun Sun)<\/td>\n		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<\/a>]<\/span><\/p>\n

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<\/a>]<\/span><\/p>\n

15:05-15:30 Julius Adelt, Daniel Brettschneider and Paula Herber, Reusable Contracts for Safe Integration of Reinforcement Learning in Hybrid Systems [Video<\/a>]<\/span><\/td>\n<\/tr>\n

Beijing 15:30-15:45
\nParis 09:30-09:45
\nSan Francisco 00:30-00:45<\/td>\n		Break<\/td>\n<\/tr>\n
Beijing 15:45-17:15
\nParis 09:45-11:15
\nSan Francisco 00:45-02:15<\/td>\n		Program analysis and verification
\n(Chair: Taolue Chen)<\/td>\n		15:45-16:00 S\u00f6ren Tempel, Vladimir Herdt and Rolf Drechsler, SISL: Concolic Testing of Structured Binary Input Formats via Partial Specification [Video<\/a>]<\/span><\/p>\n

16:00-16:25 Sanjana Singh, Divyanjali Sharma, Ishita Jaju and Subodh Sharma, Fence Synthesis for the C11 Memory Model [Video<\/a>]<\/span><\/p>\n

16:25-16:50 Anand Yeolekar, Ravindra Metta, Clara Hobbs and Samarjit Chakraborty, Checking Scheduling-induced Violations of Control Safety Properties [Video<\/a>]<\/span><\/p>\n

16:50-17:15 Hannes Kallwies, Martin Leucker and Cesar Sanchez, Symbolic Runtime Verification for Monitoring under Uncertainties and Assumptions [Video<\/a>]<\/span><\/td>\n<\/tr>\n

<\/td>\n<\/td>\n<\/td>\n<\/tr>\n
Beijing 22:00-22:10
\nParis 16:00-16:10
\nSan Francisco 07:00-07:10<\/td>\n		Advertisement for ATVA 2023<\/td>\n<\/tr>\n
Beijing 22:10-23:10
\nParis 16:10-17:10
\nSan Francisco 07:10-08:10<\/td>\n		Keynote II
\n(Chair: Naijun Zhan)<\/td>\n		Xinyu Feng,
\nCompositional Reasoning about Concurrent Randomized Programs<\/a>
\n[Video<\/a>]<\/span><\/td>\n<\/tr>\n
Beijing 23:10-00:25
\nParis 17:10-18:25
\nSan Francisco 08:10-09:25<\/td>\n		SMT and verification
\n(Chair: Philipp Rummer)<\/td>\n		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<\/a>]<\/span><\/p>\n

23:35-00:00 Alessandro Cimatti, Alberto Griggio and Gianluca Redondi, Verification of SMT Systems with Quantifiers [Video<\/a>]<\/span><\/p>\n

00:00-00:25 Jiong Yang, Supratik Chakraborty and Kuldeep S. Meel, Projected Model Counting: Beyond Independent Support [Video<\/a>]<\/span><\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n

October 27th<\/sup>, 2022.<\/h1>\n\n\n\n\n<\/colgroup>\n\n\n\n\n\n\n\n\n\n\n
Time<\/th>\nSession<\/th>\nTalks<\/th>\n<\/tr>\n<\/thead>\n
Beijing 13:00-14:00
\nParis 07:00-08:00
\nSan Francisco 22:00-23:00<\/td>\n		Keynote III
\n(Chair: Ahmed Bouajjani)<\/td>\n		Shaz Qadeer,
\nThe Civl Verifier<\/a>
\n[Video<\/a>]<\/span><\/td>\n<\/tr>\n
Beijing 14:00-15:05
\nParis 08:00-09:05
\nSan Francisco 23:00-00:05<\/td>\n		Automata and Applications
\n(Chair: Zhilin Wu)<\/td>\n		14:00-14:25 Bader Abu Radi and Orna Kupferman, Minimization of Automata for Liveness Languages [Video<\/a>]<\/span><\/p>\n

14:25-14:50 Norine Coenen, Bernd Finkbeiner, Hadar Frenkel, Christopher Hahn, Niklas Metzger and Julian Siber, Temporal Causality in Reactive Systems [Video<\/a>]<\/span><\/p>\n

14:50-15:05 Peter Gj\u00f8l Jensen, Stefan Schmid, Morten Konggaard Schou and Jiri Srba, PDAAAL: A Library for Reachability Analysis of Weighted Pushdown Systems [Video<\/a>]<\/span><\/td>\n<\/tr>\n

Beijing 15:05-15:20
\nParis 09:05-09:20
\nSan Francisco 00:05-00:20<\/td>\n		Break<\/td>\n<\/tr>\n
Beijing 15:20-16:35
\nParis 09:20-10:35
\nSan Francisco 00:20-01:35<\/td>\n		Active learning
\n(Chair: Yu-Fang Chen)<\/td>\n		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<\/a>]<\/span><\/p>\n

15:45-16:10 Runqing Xu, Jie An and Bohua Zhan, Active Learning of One-Clock Timed Automata using Constraint Solving [Video<\/a>]<\/span><\/p>\n

16:10-16:35 Dana Fisman and Sagi Saadon, Learning and Characterizing Fully-Ordered Lattice Automata [Video<\/a>]<\/span><\/td>\n<\/tr>\n

<\/td>\n<\/td>\n<\/td>\n<\/tr>\n
Beijing 22:00-23:00
\nParis 16:00-17:00
\nSan Francisco 07:00-08:00<\/td>\n		Keynote IV
\n(Chair: Orna Kupferman)<\/td>\n		Jean-Francois Raskin,
\nSubgame Perfect Equilibrium with an Algorithmic Perspective<\/a>
\n[Video<\/a>]<\/span><\/td>\n<\/tr>\n
Beijing 23:00-00:20
\nParis 17:00-18:20
\nSan Francisco 08:00-09:20<\/td>\n		Probabilistic and stochastic systems
\n(Chair: David Jansen)<\/td>\n		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<\/a>]<\/span><\/p>\n

23:25-23:50 Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi and Dominik Wojtczak, Alternating Good-for-MDPs Automata [Video<\/a>]<\/span><\/p>\n

23:50-00:05 Tobias Meggendorfer, PET \u2013 Partial Exploration Tool for Probabilistic Verification [Video<\/a>]<\/span><\/p>\n

00:05-00:20 Martijn Goorden, Peter Gj\u00f8l Jensen, Kim Guldstrand Larsen, Mihhail Samusev, Jiri Srba and Guohan Zhao, STOMPC: Stochastic Model-Predictive Control with Uppaal Stratego [Video<\/a>]<\/span><\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n

October 28th<\/sup>, 2022.<\/h1>\n\n\n\n\n<\/colgroup>\n\n\n\n\n\n\n\n\n
Time<\/th>\nSession<\/th>\nTalks<\/th>\n<\/tr>\n<\/thead>\n
Beijing 13:00-14:00
\nParis 07:00-08:00
\nSan Francisco 22:00-23:00<\/td>\n		Keynote V
\n(Chair: Lukas Holik)<\/td>\n		Mohamed Faouzi Atig,
\nFlattening String Constraints<\/a>
\n[Video<\/a>]<\/span><\/td>\n<\/tr>\n
Beijing 14:00-15:15
\nParis 08:00-09:15
\nSan Francisco 23:00-00:15<\/td>\n		Synthesis and repair
\n(Chair: Fei He)<\/td>\n		14:00-14:25 Miriam Garc\u00eda Soto, Thomas Henzinger and Christian Schilling, Synthesis of Parametric Hybrid Automata from Time Series [Video<\/a>]<\/span><\/p>\n

14:25-14:50 Vrunda Dave, Krishna S, Vishnu Murali and Ashutosh Trivedi, Optimal Repair For Omega-regular Properties [Video<\/a>]<\/span><\/p>\n

14:50-15:15 Reiya Noguchi, Ocan Sankur, Thierry J\u00e9ron, Nicolas Markey and David Mentr\u00e9, Repairing Real-Time Requirements [Video<\/a>]<\/span><\/td>\n<\/tr>\n

Beijing 15:15-15:30
\nParis 09:15-09:30
\nSan Francisco 00:15-00:30<\/td>\n		Break<\/td>\n<\/tr>\n
Beijing 15:30-16:35
\nParis 09:30-10:35
\nSan Francisco 00:30-01:35<\/td>\n		Verification of neural networks
\n(Chair: Youcheng Sun)<\/td>\n		15:30-15:45 Matan Ostrovsky, Clark Barrett and Guy Katz, An Abstraction-Refinement Approach to Verifying Convolutional Neural Networks [Video<\/a>]<\/span><\/p>\n

15:45-16:10 Chih-Hong Cheng, Changshun Wu, Emmanouil Seferis and Saddek Bensalem, Prioritizing Corners in OoD Detectors via Symbolic String Manipulation [Video<\/a>]<\/span><\/p>\n

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<\/a>]<\/span><\/td>\n<\/tr>\n

Beijing 16:35-16:45
\nParis 10:35-10:45
\nSan Francisco 01:35-01:45<\/td>\n		Closing: Announcement of Best Paper Award<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n","protected":false},"excerpt":{"rendered":"

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…<\/p>\n","protected":false},"author":1,"featured_media":0,"parent":0,"menu_order":0,"comment_status":"closed","ping_status":"closed","template":"","meta":{"nf_dc_page":"","footnotes":""},"class_list":["post-34","page","type-page","status-publish","hentry"],"_links":{"self":[{"href":"https:\/\/atva-conference.org\/2022\/wp-json\/wp\/v2\/pages\/34","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/atva-conference.org\/2022\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/atva-conference.org\/2022\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/atva-conference.org\/2022\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/atva-conference.org\/2022\/wp-json\/wp\/v2\/comments?post=34"}],"version-history":[{"count":5,"href":"https:\/\/atva-conference.org\/2022\/wp-json\/wp\/v2\/pages\/34\/revisions"}],"predecessor-version":[{"id":499,"href":"https:\/\/atva-conference.org\/2022\/wp-json\/wp\/v2\/pages\/34\/revisions\/499"}],"wp:attachment":[{"href":"https:\/\/atva-conference.org\/2022\/wp-json\/wp\/v2\/media?parent=34"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}