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

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