Automated Technology for Verification and Analysis: 15th International Symposium, ATVA 2017, Pune, India, October 3–6, 2017, Proceedings

Description

This book constitutes the refereed proceedings of the 15th International Symposium on Automated Technology for Verification and Analysis, ATVA 2017, held in Pune, India, in October 2017. The 22 full and 7 short papers presented in this volume were carefully reviewed and selected from 78 submissions. The book also contains one invited talk in full-paper length. The contributions are organized in topical sections named: program analysis; model checking and temporal logics; neural networks; learning and invariant synthesis; and hybrid systems and control. Front Matter ....Pages I-XIX Front Matter ....Pages 1-1 Proving Absence of Starvation by Means of Abstract Interpretation and Model Checking (Helmut Seidl, Ralf Vogler)....Pages 3-22 Front Matter ....Pages 23-23 Precise Null Pointer Analysis Through Global Value Numbering (Ankush Das, Akash Lal)....Pages 25-41 May-Happen-in-Parallel Analysis with Returned Futures (Elvira Albert, Samir Genaim, Pablo Gordillo)....Pages 42-58 JTDec: A Tool for Tree Decompositions in Soot (Krishnendu Chatterjee, Amir Kafshdar Goharshady, Andreas Pavlogiannis)....Pages 59-66 Fixing the State Budget: Approximation of Regular Languages with Small DFAs (Graeme Gange, Pierre Ganty, Peter J. Stuckey)....Pages 67-83 An Equivalence Checking Framework for Array-Intensive Programs (Kunal Banerjee, Chittaranjan Mandal, Dipankar Sarkar)....Pages 84-90 Loop Quasi-Invariant Chunk Detection (Jean-Yves Moyen, Thomas Rubiano, Thomas Seiller)....Pages 91-108 SamaTulyata: An Efficient Path Based Equivalence Checking Tool (Soumyadip Bandyopadhyay, Santonu Sarkar, Dipankar Sarkar, Chittaranjan Mandal)....Pages 109-116 Front Matter ....Pages 117-117 Tests and Refutation (Mohammad Torabi Dashti, David Basin)....Pages 119-138 The Density of Linear-Time Properties (Bernd Finkbeiner, Hazem Torfah)....Pages 139-155 HyLeak: Hybrid Analysis Tool for Information Leakage (Fabrizio Biondi, Yusuke Kawamoto, Axel Legay, Louis-Marie Traonouez)....Pages 156-163 Compositional Safety Refutation Techniques (Kumar Madhukar, Peter Schrammel, Mandayam Srivas)....Pages 164-183 Gradient-Based Variable Ordering of Decision Diagrams for Systems with Structural Units (Elvio Gilberto Amparore, Marco Beccuti, Susanna Donatelli)....Pages 184-200 Model Checking of C and C++ with DIVINE 4 (Zuzana Baranová, Jiří Barnat, Katarína Kejstová, Tadeáš Kučera, Henrich Lauko, Jan Mrázek et al.)....Pages 201-207 Dealing with Priorities and Locks for Concurrent Programs (Marcio Diaz, Tayssir Touili)....Pages 208-224 Knowledge Transfer and Information Leakage in Protocols (Abdullah Abdul Khadir, Madhavan Mukund, S. P. Suresh)....Pages 225-240 Concurrent Program Verification with Invariant-Guided Underapproximation (Sumanth Prabhu, Peter Schrammel, Mandayam Srivas, Michael Tautschnig, Anand Yeolekar)....Pages 241-248 Front Matter ....Pages 249-249 Maximum Resilience of Artificial Neural Networks (Chih-Hong Cheng, Georg Nührenberg, Harald Ruess)....Pages 251-268 Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks (Rüdiger Ehlers)....Pages 269-286 Front Matter ....Pages 287-287 Liquid Types for Array Invariant Synthesis (Manuel Montenegro, Susana Nieva, Ricardo Peña, Clara Segura)....Pages 289-306 Lifting CDCL to Template-Based Abstract Domains for Program Verification (Rajdeep Mukherjee, Peter Schrammel, Leopold Haller, Daniel Kroening, Tom Melham)....Pages 307-326 Synthesizing Invariants by Solving Solvable Loops (Steven de Oliveira, Saddek Bensalem, Virgile Prevosto)....Pages 327-343 Exploiting Partial Knowledge for Efficient Model Analysis (Nuno Macedo, Alcino Cunha, Eduardo Pessoa)....Pages 344-362 A Language-Theoretic View on Network Protocols (Pierre Ganty, Boris Köpf, Pedro Valero)....Pages 363-379 Efficient Strategy Iteration for Mean Payoff in Markov Decision Processes (Jan Křetínský, Tobias Meggendorfer)....Pages 380-399 Finding Polynomial Loop Invariants for Probabilistic Programs (Yijun Feng, Lijun Zhang, David N. Jansen, Naijun Zhan, Bican Xia)....Pages 400-416 Synthesis of Optimal Resilient Control Strategies (Christel Baier, Clemens Dubslaff, L’uboš Korenčiak, Antonín Kučera, Vojtěch Řehák)....Pages 417-434 Front Matter ....Pages 435-435 ForFET: A Formal Feature Evaluation Tool for Hybrid Systems (Antonio Anastasio Bruto da Costa, Pallab Dasgupta)....Pages 437-445 Attacking the V: On the Resiliency of Adaptive-Horizon MPC (Ashish Tiwari, Scott A. Smolka, Lukas Esterle, Anna Lukina, Junxing Yang, Radu Grosu)....Pages 446-462 The Reach-Avoid Problem for Constant-Rate Multi-mode Systems (Shankara Narayanan Krishna, Aviral Kumar, Fabio Somenzi, Behrouz Touri, Ashutosh Trivedi)....Pages 463-479 Back Matter ....Pages 481-482