![Automated technology for verification and analysis [electronic resource] : 15th International Symposium, ATVA 2017, Pune, India, October 3–6, 2017, Proceedings](https://libdoc.korea.ac.kr/dl_image/IMG/14/000000349172/INTROIMAGE/000000349172_01.JPG)
Automated technology for verification and analysis [electronic resource] : 15th International Symposium, ATVA 2017, Pune, India, October 3–6, 2017, Proceedings
| 000 | 00000cam u2200205 a 4500 | |
| 001 | 000045989628 | |
| 005 | 20190718104501 | |
| 006 | m d | |
| 007 | cr | |
| 008 | 190708s2017 sz a ob 101 0 eng d | |
| 020 | ▼a 9783319681665 | |
| 020 | ▼a 9783319681672 (e-book) | |
| 040 | ▼a 211009 ▼c 211009 ▼d 211009 | |
| 050 | 4 | ▼a QA76.9.A96 |
| 082 | 0 4 | ▼a 006.333 ▼2 23 |
| 084 | ▼a 006.333 ▼2 DDCK | |
| 090 | ▼a 006.333 | |
| 245 | 0 0 | ▼a Automated technology for verification and analysis ▼h [electronic resource] : ▼b 15th International Symposium, ATVA 2017, Pune, India, October 3–6, 2017, Proceedings / ▼c Deepak D'Souza, K. Narayan Kumar, editors. |
| 260 | ▼a Cham : ▼b Springer, ▼c c2017. | |
| 300 | ▼a 1 online resource (xix, 482 p.) : ▼b ill. | |
| 490 | 1 | ▼a Programming and Software Engineering ; ▼v 10482 |
| 500 | ▼a Title from e-Book title page. | |
| 504 | ▼a Includes bibliographical references and index. | |
| 505 | 0 | ▼a 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. |
| 520 | ▼a 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. | |
| 530 | ▼a Issued also as a book. | |
| 538 | ▼a Mode of access: World Wide Web. | |
| 650 | 0 | ▼a Automatic theorem proving ▼v Congresses. |
| 650 | 0 | ▼a Artificial intelligence ▼v Congresses. |
| 700 | 1 | ▼a D'Souza, Deepak. |
| 700 | 1 | ▼a Narayan Kumar, K. |
| 711 | 2 | ▼a ATVA (Symposium) ▼n (15th : ▼d 2017 : ▼c Pune, India). |
| 830 | 0 | ▼a Programming and Software Engineering ; ▼v 10482. |
| 856 | 4 0 | ▼u https://oca.korea.ac.kr/link.n2s?url=https://doi.org/10.1007/978-3-319-68167-2 |
| 945 | ▼a KLPA | |
| 991 | ▼a E-Book(소장) |
소장정보
| No. | 소장처 | 청구기호 | 등록번호 | 도서상태 | 반납예정일 | 예약 | 서비스 |
|---|---|---|---|---|---|---|---|
| No. 1 | 소장처 중앙도서관/e-Book 컬렉션/ | 청구기호 CR 006.333 | 등록번호 E14015170 | 도서상태 대출불가(열람가능) | 반납예정일 | 예약 | 서비스 |
컨텐츠정보
책소개
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.
정보제공 :
목차
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.