Computer Aided Verification: 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part I

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