Automated Technology for Verification and Analysis: 16th International Symposium, ATVA 2018, Los Angeles, CA, USA, October 7-10, 2018, Proceedings

Front Matter ....Pages I-XIII
Front Matter ....Pages 1-1
 DeepSafe: A Data-Driven Approach for Assessing Robustness of Neural Networks  (Divya Gopinath, Guy Katz, Corina S. Păsăreanu, Clark Barrett)....Pages 3-19
 Formal Specification for Deep Neural Networks  (Sanjit A. Seshia, Ankush Desai, Tommaso Dreossi, Daniel J. Fremont, Shromona Ghosh, Edward Kim et al.)....Pages 20-34
Front Matter ....Pages 35-35
 Optimal Proofs for Linear Temporal Logic on Lasso Words  (David Basin, Bhargav Nagaraja Bhatt, Dmitriy Traytel)....Pages 37-55
 What’s to Come is Still Unsure  (Mingshuai Chen, Martin Fränzle, Yangjia Li, Peter N. Mosaad, Naijun Zhan)....Pages 56-74
 A Formally Verified Motion Planner for Autonomous Vehicles  (Albert Rizaldi, Fabian Immler, Bastian Schürmann, Matthias Althoff)....Pages 75-90
 Robustness Testing of Intermediate Verifiers  (YuTing Chen, Carlo A. Furia)....Pages 91-108
 Simulation Algorithms for Symbolic Automata  (Lukáš Holík, Ondřej Lengál, Juraj Síč, Margus Veanes, Tomáš Vojnar)....Pages 109-125
 Quantitative Projection Coverage for Testing ML-enabled Autonomous Systems  (Chih-Hong Cheng, Chung-Hao Huang, Hirotoshi Yasuoka)....Pages 126-142
 Recursive Online Enumeration of All Minimal Unsatisfiable Subsets  (Jaroslav Bendík, Ivana Černá, Nikola Beneš)....Pages 143-159
 Synthesis in pMDPs: A Tale of 1001 Parameters  (Murat Cubuktepe, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen, Ufuk Topcu)....Pages 160-176
 Temporal Logic Verification of Stochastic Systems Using Barrier Certificates  (Pushpak Jagtap, Sadegh Soudjani, Majid Zamani)....Pages 177-193
 Bisimilarity Distances for Approximate Differential Privacy  (Dmitry Chistikov, Andrzej S. Murawski, David Purser)....Pages 194-210
 A Symbolic Algorithm for Lazy Synthesis of Eager Strategies  (Swen Jacobs, Mouhammad Sakr)....Pages 211-227
 Modular Verification of Concurrent Programs via Sequential Model Checking  (Dan Rasin, Orna Grumberg, Sharon Shoham)....Pages 228-247
 Quantifiers on Demand  (Arie Gurfinkel, Sharon Shoham, Yakir Vizel)....Pages 248-266
 Signal Convolution Logic  (Simone Silvetti, Laura Nenzi, Ezio Bartocci, Luca Bortolussi)....Pages 267-283
 Efficient Symbolic Representation of Convex Polyhedra in High-Dimensional Spaces  (Bernard Boigelot, Isabelle Mainz)....Pages 284-299
 Accelerated Model Checking of Parametric Markov Chains  (Paul Gainer, Ernst Moritz Hahn, Sven Schewe)....Pages 300-316
 Continuous-Time Markov Decisions Based on Partial Exploration  (Pranav Ashok, Yuliya Butkova, Holger Hermanns, Jan Křetínský)....Pages 317-334
 A Fragment of Linear Temporal Logic for Universal Very Weak Automata  (Keerthi Adabala, Rüdiger Ehlers)....Pages 335-351
 Quadratic Word Equations with Length Constraints, Counter Systems, and Presburger Arithmetic with Divisibility  (Anthony W. Lin, Rupak Majumdar)....Pages 352-369
 Round-Bounded Control of Parameterized Systems  (Benedikt Bollig, Mathieu Lehaut, Nathalie Sznajder)....Pages 370-386
 PSense: Automatic Sensitivity Analysis for Probabilistic Programs  (Zixin Huang, Zhenbang Wang, Sasa Misailovic)....Pages 387-403
 Information Leakage in Arbiter Protocols  (Nestan Tsiskaridze, Lucas Bang, Joseph McMahan, Tevfik Bultan, Timothy Sherwood)....Pages 404-421
 Neural State Classification for Hybrid Systems  (Dung Phan, Nicola Paoletti, Timothy Zhang, Radu Grosu, Scott A. Smolka, Scott D. Stoller)....Pages 422-440
 Bounded Synthesis of Reactive Programs  (Carsten Gerstacker, Felix Klein, Bernd Finkbeiner)....Pages 441-457
 Maximum Realizability for Linear Temporal Logic Specifications  (Rayna Dimitrova, Mahsa Ghasemi, Ufuk Topcu)....Pages 458-475
 Ranking and Repulsing Supermartingales for Reachability in Probabilistic Programs  (Toru Takisaka, Yuichiro Oyabu, Natsuki Urabe, Ichiro Hasuo)....Pages 476-493
 Bounded Synthesis of Register Transducers  (Ayrat Khalimov, Benedikt Maderbacher, Roderick Bloem)....Pages 494-510
Front Matter ....Pages 511-511
 EthIR: A Framework for High-Level Analysis of Ethereum Bytecode  (Elvira Albert, Pablo Gordillo, Benjamin Livshits, Albert Rubio, Ilya Sergey)....Pages 513-520
 MGHyper: Checking Satisfiability of HyperLTL Formulas Beyond the \\(\\exists ^*\\forall ^*\\) Fragment  (Bernd Finkbeiner, Christopher Hahn, Tobias Hans)....Pages 521-527
 Verifying Rust Programs with SMACK  (Marek Baranowski, Shaobo He, Zvonimir Rakamarić)....Pages 528-535
 \\(\\mathcal {S}\\)BIP 2.0: Statistical Model Checking Stochastic Real-Time Systems  (Braham Lotfi Mediouni, Ayoub Nouri, Marius Bozga, Mahieddine Dellabani, Axel Legay, Saddek Bensalem)....Pages 536-542
 Owl: A Library for \\(\\omega \\)-Words, Automata, and LTL  (Jan Křetínský, Tobias Meggendorfer, Salomon Sickert)....Pages 543-550
 EVE: A Tool for Temporal Equilibrium Analysis  (Julian Gutierrez, Muhammad Najib, Giuseppe Perelli, Michael Wooldridge)....Pages 551-557
Back Matter ....Pages 559-560