Automated Technology for Verification and Analysis: 18th International Symposium, ATVA 2020, Hanoi, Vietnam, October 19–23, 2020, Proceedings

Front Matter ....Pages i-xiv
Front Matter ....Pages 1-1
 First-Order Timed Runtime Verification Using BDDs  (Klaus Havelund, Doron Peled)....Pages 3-24
 Verified Textbook Algorithms  (Tobias Nipkow, Manuel Eberl, Maximilian P. L. Haslbeck)....Pages 25-53
Front Matter ....Pages 55-55
 Verifying Recurrent Neural Networks Using Invariant Inference  (Yuval Jacoby, Clark Barrett, Guy Katz)....Pages 57-74
 NeuralExplorer: State Space Exploration of Closed Loop Control Systems Using Neural Networks  (Manish Goyal, Parasara Sridhar Duggirala)....Pages 75-91
 DeepAbstract: Neural Network Abstraction for Accelerating Verification  (Pranav Ashok, Vahid Hashemi, Jan Křetínský, Stefanie Mohr)....Pages 92-107
 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, Dominik Wojtczak)....Pages 108-124
Front Matter ....Pages 125-125
 Practical “Paritizing” of Emerson-Lei Automata  (Florian Renkin, Alexandre Duret-Lutz, Adrien Pommellet)....Pages 127-143
 Complexity of Verification and Synthesis of Threshold Automata  (A. R. Balasubramanian, Javier Esparza, Marijana Lazić)....Pages 144-160
 On (I/O)-Aware Good-For-Games Automata  (Rachel Faran, Orna Kupferman)....Pages 161-178
 Urgent Partial Order Reduction for Extended Timed Automata  (Kim G. Larsen, Marius Mikučionis, Marco Muñiz, Jiří Srba)....Pages 179-195
 Eliminating Message Counters in Threshold Automata  (Ilina Stoilkovska, Igor Konnov, Josef Widder, Florian Zuleger)....Pages 196-212
Front Matter ....Pages 213-213
 Context-Aware Temporal Logic for Probabilistic Systems  (Mahmoud Elfar, Yu Wang, Miroslav Pajic)....Pages 215-232
 Multi-head Monitoring of Metric Dynamic Logic  (Martin Raszyk, David Basin, Dmitriy Traytel)....Pages 233-250
Front Matter ....Pages 251-251
 Faster Algorithms for Quantitative Analysis of MCs and MDPs with Small Treewidth  (Ali Asadi, Krishnendu Chatterjee, Amir Kafshdar Goharshady, Kiarash Mohammadi, Andreas Pavlogiannis)....Pages 253-270
 Robustness Verification for Classifier Ensembles  (Dennis Gross, Nils Jansen, Guillermo A. Pérez, Stephan Raaijmakers)....Pages 271-287
 Verification of Indefinite-Horizon POMDPs  (Alexander Bork, Sebastian Junges, Joost-Pieter Katoen, Tim Quatmann)....Pages 288-304
 Verification of a Generative Separation Kernel  (Inzemamul Haque, D. D’Souza, P. Habeeb, A. Kundu, Ganesh Babu)....Pages 305-322
Front Matter ....Pages 323-323
 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 et al.)....Pages 325-342
 From Checking to Inference: Actual Causality Computations as Optimization Problems  (Amjad Ibrahim, Alexander Pretschner)....Pages 343-359
 Boosting Sequential Consistency Checking Using Saturation  (Rachid Zennou, Mohamed Faouzi Atig, Ranadeep Biswas, Ahmed Bouajjani, Constantin Enea, Mohammed Erradi)....Pages 360-376
 Parallel Graph-Based Stateless Model Checking  (Magnus Lång, Konstantinos Sagonas)....Pages 377-393
 Model Checking Branching Properties on Petri Nets with Transits  (Bernd Finkbeiner, Manuel Gieseking, Jesko Hecking-Harbusch, Ernst-Rüdiger Olderog)....Pages 394-410
Front Matter ....Pages 411-411
 Explainable Reactive Synthesis  (Tom Baumeister, Bernd Finkbeiner, Hazem Torfah)....Pages 413-428
 Robust Controller Synthesis for Duration Calculus  (Kalyani Dole, Ashutosh Gupta, Shankara Narayanan Krishna)....Pages 429-446
 Dependency-Based Compositional Synthesis  (Bernd Finkbeiner, Noemi Passing)....Pages 447-463
Front Matter ....Pages 465-465
 Proving Non-inclusion of Büchi Automata Based on Monte Carlo Sampling  (Yong Li, Andrea Turrini, Xuechao Sun, Lijun Zhang)....Pages 467-483
 Probabilistic Hyperproperties of Markov Decision Processes  (Rayna Dimitrova, Bernd Finkbeiner, Hazem Torfah)....Pages 484-500
 Minimal Witnesses for Probabilistic Timed Automata  (Simon Jantsch, Florian Funke, Christel Baier)....Pages 501-517
 Probabilistic Hyperproperties with Nondeterminism  (Erika Ábrahám, Ezio Bartocci, Borzoo Bonakdarpour, Oyendrila Dobe)....Pages 518-534
Front Matter ....Pages 535-535
 ReachNN*: A Tool for Reachability Analysis of Neural-Network Controlled Systems  (Jiameng Fan, Chao Huang, Xin Chen, Wenchao Li, Qi Zhu)....Pages 537-542
 RVX - A Tool for Concolic Testing of Embedded Binaries Targeting RISC-V Platforms  (Vladimir Herdt, Daniel Große, Rolf Drechsler)....Pages 543-549
 Peregrine 2.0: Explaining Correctness of Population Protocols Through Stage Graphs  (Javier Esparza, Martin Helfrich, Stefan Jaax, Philipp J. Meyer)....Pages 550-556
 DG: Analysis and Slicing of LLVM Bitcode  (Marek Chalupa)....Pages 557-563
 RTAMT: Online Robustness Monitors from STL  (Dejan Ničković, Tomoya Yamaguchi)....Pages 564-571
Back Matter ....Pages 573-574