Computer Aided Verification: 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part I (Lecture Notes in Computer Science Book 11561)

This open access two-volume set LNCS 11561 and 11562 constitutes the refereed proceedings of the 31st International Conference on Computer Aided Verification, CAV 2019, held in New York City, USA, in July 2019. The 52 full papers presented together with 13 tool papers and 2 case studies, were carefully reviewed and selected from 258 submissions. The papers were organized in the following topical sections: Part I: automata and timed systems; security and hyperproperties; synthesis; model checking; cyber-physical systems and machine learning; probabilistic systems, runtime techniques; dynamical, hybrid, and reactive systems; Part II: logics, decision procedures; and solvers; numerical programs; verification; distributed systems and networks; verification and invariants; and concurrency. Front Matter ....Pages i-xix Front Matter ....Pages 1-1 Symbolic Register Automata (Loris D’Antoni, Tiago Ferreira, Matteo Sammartino, Alexandra Silva)....Pages 3-21 Abstraction Refinement Algorithms for Timed Automata (Victor Roussanaly, Ocan Sankur, Nicolas Markey)....Pages 22-40 Fast Algorithms for Handling Diagonal Constraints in Timed Automata (Paul Gastin, Sayan Mukherjee, B. Srivathsan)....Pages 41-59 Safety and Co-safety Comparator Automata for Discounted-Sum Inclusion (Suguman Bansal, Moshe Y. Vardi)....Pages 60-78 Clock Bound Repair for Timed Systems (Martin Kölbl, Stefan Leue, Thomas Wies)....Pages 79-96 Verifying Asynchronous Interactions via Communicating Session Automata (Julien Lange, Nobuko Yoshida)....Pages 97-117 Front Matter ....Pages 119-119 Verifying Hyperliveness (Norine Coenen, Bernd Finkbeiner, César Sánchez, Leander Tentrup)....Pages 121-139 Quantitative Mitigation of Timing Side Channels (Saeid Tizpaz-Niari, Pavol Černý, Ashutosh Trivedi)....Pages 140-160 Property Directed Self Composition (Ron Shemer, Arie Gurfinkel, Sharon Shoham, Yakir Vizel)....Pages 161-179 Security-Aware Synthesis Using Delayed-Action Games (Mahmoud Elfar, Yu Wang, Miroslav Pajic)....Pages 180-199 Automated Hypersafety Verification (Azadeh Farzan, Anthony Vandikas)....Pages 200-218 Automated Synthesis of Secure Platform Mappings (Eunsuk Kang, Stéphane Lafortune, Stavros Tripakis)....Pages 219-237 Front Matter ....Pages 239-239 Synthesizing Approximate Implementations for Unrealizable Specifications (Rayna Dimitrova, Bernd Finkbeiner, Hazem Torfah)....Pages 241-258 Quantified Invariants via Syntax-Guided Synthesis (Grigory Fedyukovich, Sumanth Prabhu, Kumar Madhukar, Aarti Gupta)....Pages 259-277 Efficient Synthesis with Probabilistic Constraints (Samuel Drews, Aws Albarghouthi, Loris D’Antoni)....Pages 278-296 Membership-Based Synthesis of Linear Hybrid Automata (Miriam García Soto, Thomas A. Henzinger, Christian Schilling, Luka Zeleznik)....Pages 297-314 Overfitting in Synthesis: Theory and Practice (Saswat Padhi, Todd Millstein, Aditya Nori, Rahul Sharma)....Pages 315-334 Proving Unrealizability for Syntax-Guided Synthesis (Qinheping Hu, Jason Breck, John Cyphert, Loris D’Antoni, Thomas Reps)....Pages 335-352 Front Matter ....Pages 353-353 BMC for Weak Memory Models: Relation Analysis for Compact SMT Encodings (Natalia Gavrilenko, Hernán Ponce-de-León, Florian Furbach, Keijo Heljanko, Roland Meyer)....Pages 355-365 When Human Intuition Fails: Using Formal Methods to Find an Error in the “Proof” of a Multi-agent Protocol (Jennifer A. Davis, Laura R. Humphrey, Derek B. Kingston)....Pages 366-375 Extending nuXmv with Timed Transition Systems and Timed Temporal Properties (Alessandro Cimatti, Alberto Griggio, Enrico Magnago, Marco Roveri, Stefano Tonetta)....Pages 376-386 Cerberus-BMC: A Principled Reference Semantics and Exploration Tool for Concurrent and Sequential C (Stella Lau, Victor B. F. Gomes, Kayvan Memarian, Jean Pichon-Pharabod, Peter Sewell)....Pages 387-397 Front Matter ....Pages 399-399 Multi-armed Bandits for Boolean Connectives in Hybrid System Falsification (Zhenya Zhang, Ichiro Hasuo, Paolo Arcaini)....Pages 401-420 StreamLAB: Stream-based Monitoring of Cyber-Physical Systems (Peter Faymonville, Bernd Finkbeiner, Malte Schledjewski, Maximilian Schwenger, Marvin Stenger, Leander Tentrup et al.)....Pages 421-431 VerifAI: A Toolkit for the Formal Design and Analysis of Artificial Intelligence-Based Systems (Tommaso Dreossi, Daniel J. Fremont, Shromona Ghosh, Edward Kim, Hadi Ravanbakhsh, Marcell Vazquez-Chanlatte et al.)....Pages 432-442 The Marabou Framework for Verification and Analysis of Deep Neural Networks (Guy Katz, Derek A. Huang, Duligur Ibeling, Kyle Julian, Christopher Lazarus, Rachel Lim et al.)....Pages 443-452 Front Matter ....Pages 453-453 Probabilistic Bisimulation for Parameterized Systems (Chih-Duo Hong, Anthony W. Lin, Rupak Majumdar, Philipp Rümmer)....Pages 455-474 Semi-quantitative Abstraction and Analysis of Chemical Reaction Networks (Milan Češka, Jan Křetínský)....Pages 475-496 PAC Statistical Model Checking for Markov Decision Processes and Stochastic Games (Pranav Ashok, Jan Křetínský, Maximilian Weininger)....Pages 497-519 Symbolic Monitoring Against Specifications Parametric in Time and Data (Masaki Waga, Étienne André, Ichiro Hasuo)....Pages 520-539 STAMINA: STochastic Approximate Model-Checker for INfinite-State Analysis (Thakur Neupane, Chris J. Myers, Curtis Madsen, Hao Zheng, Zhen Zhang)....Pages 540-549 Front Matter ....Pages 551-551 Local and Compositional Reasoning for Optimized Reactive Systems (Mitesh Jain, Panagiotis Manolios)....Pages 553-571 Robust Controller Synthesis in Timed Büchi Automata: A Symbolic Approach (Damien Busatto-Gaston, Benjamin Monmege, Pierre-Alain Reynier, Ocan Sankur)....Pages 572-590 Flexible Computational Pipelines for Robust Abstraction-Based Control Synthesis (Eric S. Kim, Murat Arcak, Sanjit A. Seshia)....Pages 591-608 Temporal Stream Logic: Synthesis Beyond the Bools (Bernd Finkbeiner, Felix Klein, Ruzica Piskac, Mark Santolucito)....Pages 609-629 Run-Time Optimization for Learned Controllers Through Quantitative Games (Guy Avni, Roderick Bloem, Krishnendu Chatterjee, Thomas A. Henzinger, Bettina Könighofer, Stefan Pranger)....Pages 630-649 Taming Delays in Dynamical Systems (Shenghua Feng, Mingshuai Chen, Naijun Zhan, Martin Fränzle, Bai Xue)....Pages 650-669 Back Matter ....Pages 671-673