Automated Technology for Verification and Analysis: 15th International Symposium, ATVA 2017, Pune, I

Invited Talk: Proving Absence of Starvation by Means of Abstract Interpretation and Model-checking.- Program Analysis.- Precise Null Pointer Analysis Through Global Value Numbering.- May-Happen-in-Parallel Analysis with Returned Futures.- JTDec: A Tool for Tree Decompositions in Soot.- Fixing the State Budget: Approximation of Regular Languages with Small DFAs.- An Equivalence Checking Framework for Array-Intensive Programs.-Loop Quasi-Invariant Chunk Detection.- SamaTulyata: An Efficient Path Based Equivalence Checking Tool.- Model Checking and Temporal Logics.- Tests and Refutation.- The Density of Linear-time Properties.- HyLeak: Hybrid Analysis Tool for Information Leakage.- Compositional Safety Refutation Techniques.- Gradient-based variable ordering of Decision Diagrams for systems with structural units.- Model Checking of C and C++ with DIVINE 4 (Tool Paper).- Dealing with priorities and locks for concurrent programs.- Knowledge transfer and information leakage in protocols.- Concurrent Program Verification With Invariant-guided Underapproximation.- Neural Networks.- Maximum Resilience of Artificial Neural Networks.- Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks.- Learning and Invariant Synthesis.- Liquid Types for Array Invariant Synthesis.- Lifting CDCL to Template-based Abstract Domains for Program Verification.- Synthesizing invariants by solving solvable loops.- Requirements and Specifications Exploiting Partial Knowledge for Efficient Model Analysis.- A Language-theoretic View on Network Protocols.- Probabilistic Systems Efficient Strategy Iteration for Mean Payoff in Markov Decision Processes.- Finding Polynomial Loop Invariants for Probabilistic Programs.- Synthesis of Optimal Resilient Control Strategies.- Hybrid Systems and Control.- ForFET: A Formal Feature Evaluation Tool for Hybrid Systems.- Attacking the V: On the Resiliency of Adaptive-Horizon MPC.- The Reach-Avoid Problem for Constant-Rate Multi-Mode Systems.