LEADER 05225nam 22007815 450 001 9910483596703321 005 20251225205250.0 010 $a3-319-68167-2 024 7 $a10.1007/978-3-319-68167-2 035 $a(CKB)4100000000881943 035 $a(DE-He213)978-3-319-68167-2 035 $a(MiAaPQ)EBC6285240 035 $a(MiAaPQ)EBC5591611 035 $a(Au-PeEL)EBL5591611 035 $a(OCoLC)1005921555 035 $a(PPN)220121206 035 $a(EXLCZ)994100000000881943 100 $a20171003d2017 u| 0 101 0 $aeng 135 $aurnn|008mamaa 181 $ctxt$2rdacontent 182 $cc$2rdamedia 183 $acr$2rdacarrier 200 10$aAutomated Technology for Verification and Analysis $e15th International Symposium, ATVA 2017, Pune, India, October 3?6, 2017, Proceedings /$fedited by Deepak D'Souza, K. Narayan Kumar 205 $a1st ed. 2017. 210 1$aCham :$cSpringer International Publishing :$cImprint: Springer,$d2017. 215 $a1 online resource (XIX, 482 p. 106 illus.) 225 1 $aProgramming and Software Engineering,$x2945-9168 ;$v10482 311 08$a3-319-68166-4 327 $aInvited 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. 330 $aThis 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. 410 0$aProgramming and Software Engineering,$x2945-9168 ;$v10482 606 $aSoftware engineering 606 $aCompilers (Computer programs) 606 $aComputer engineering 606 $aComputer networks 606 $aComputers 606 $aComputer science 606 $aArtificial intelligence 606 $aSoftware Engineering 606 $aCompilers and Interpreters 606 $aComputer Engineering and Networks 606 $aComputing Milieux 606 $aTheory of Computation 606 $aArtificial Intelligence 615 0$aSoftware engineering. 615 0$aCompilers (Computer programs). 615 0$aComputer engineering. 615 0$aComputer networks. 615 0$aComputers. 615 0$aComputer science. 615 0$aArtificial intelligence. 615 14$aSoftware Engineering. 615 24$aCompilers and Interpreters. 615 24$aComputer Engineering and Networks. 615 24$aComputing Milieux. 615 24$aTheory of Computation. 615 24$aArtificial Intelligence. 676 $a004.015113 702 $aD'Souza$b Deepak$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aNarayan Kumar$b K$4edt$4http://id.loc.gov/vocabulary/relators/edt 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a9910483596703321 996 $aAutomated Technology for Verification and Analysis$9772478 997 $aUNINA