Automated technology for verification and analysis : 14th International Symposium, ATVA 2016, Chiba, Japan, October 17-20, 2016, Proceedings /: 14th International Symposium, ATVA 2016, Chiba, Japan, October 17-20, 2016, Proceedings. (2016)

• Record Type: Book
• Other Titles: ATVA 2016
• Further Information: Note: Cyrille Artho, Axel Legay, Doron Peled (eds.).
• Editors: Artho, Cyrille; Legay, Axel; Peled, Doron A, 1962-
• Other Names: ATVA (Symposium), 14th
• Contents: Intro; Preface; Organization; Contents; Keynote; Synthesizing and Completely Testing Hardware Based on Templates Through Small Numbers of Test Patterns; 1 QBF Formulation; 2 The Base Algorithm; 3 Automatic Test Pattern Generation (ATPG) for General Multiple Faults; 4 Concluding Remarks; References; Markov Models, Chains, and Decision Processes; Approximate Policy Iteration for Markov Decision Processes via Quantitative Adaptive Aggregations; 1 Introduction; 2 Notations and Problem Setup; 3 New Approximate Policy Iteration; 3.1 State-Space Aggregation for MDPs 3.2 Approximate Policy Iteration: Quantification and Use of Error Bounds3.3 Tighter and Computationally Faster Matrix Bounds; 4 Experimental Evaluation; 4.1 Fixed Number of Policy Updates and Evaluations; 4.2 Convergence of the Approximate Scheme; 4.3 Discussion of the Experimental Results; 5 Conclusions and Future Work; References; Optimizing the Expected Mean Payoff in Energy Markov Decision Processes; 1 Introduction; 2 Preliminaries; 3 The Results; 3.1 Strongly Connected and Pumpable EMDPs; 3.2 General EMDPs; References; Parameter Synthesis for Markov Models: Faster Than Ever 1 Introduction2 Preliminaries; 2.1 Probabilistic Models; 2.2 Properties of Interest; 3 Regional Model Checking of Markov Chains; 3.1 Regions; 3.2 Relaxation; 3.3 Substituting Parameters with Nondeterminism; 4 Regional Checking of Models with Nondeterminism; 5 Parameter Synthesis; 6 Experimental Evaluation; 7 Conclusion; References; Bounded Model Checking for Probabilistic Programs; 1 Introduction; 2 Preliminaries; 2.1 Distributions and Polynomials; 2.2 Probabilistic Models; 2.3 Conditional Probabilistic Guarded Command Language; 2.4 Operational Semantics for Probabilistic Programs 3 Bounded Model Checking for Probabilistic Programs3.1 Growing Expectations; 3.2 Model Checking; 4 Evaluation; 5 Conclusion and Future Work; References; Counter Systems, Automata; How Hard is It to Verify Flat Affine Counter Systems with the Finite Monoid Property?; 1 Introduction; 2 Counter Systems and Their Decision Problems; 2.1 Counter Systems; 2.2 Decision Problems; 3 A Hardness Result; 4 Bounding the Number of Cycle Iterations; 5 The Complexities of Decision Problems for ASdffm; 5.1 Reachability is 2P; 5.2 PLTL Model Checking is 2P; 5.3 FO Model Checking is PSPACE-complete; References Solving Language Equations Using Flanked Automata1 Introduction; 2 Notations and Definitions; 3 Complexity Results for Basic Problems; 4 Closure Properties of Flanked Automata; 5 Succinctness of Flanked Automata; 6 A Simple Use Case for FFA; 7 Related Work; 8 Conclusion; References; Spot 2.0 -- A Framework for LTL and -Automata Manipulation; 1 Introduction; 2 Command-Line Tools; 3 The Python Interface; 4 Model Checkers Built Using Spot; References; MoChiBA: Probabilistic LTL Model Checking Using Limit-Deterministic Büchi Automata; 1 Introduction; 2 Overview of the Algorithm
• Publisher Details: Cham, Switzerland : Springer
• Publication Date: 2016
• Extent: 1 online resource (xi, 530 pages), illustrations
• Subjects: 006.3/33; Computer science; Automatic theorem proving -- Congresses; Artificial intelligence -- Congresses; Artificial intelligence; Automatic theorem proving; Computer Science; Software Engineering; Programming Languages, Compilers, Interpreters; Logics and Meanings of Programs; Mathematical Logic and Formal Languages; Artificial Intelligence (incl. Robotics); Programming Techniques; Computers -- Programming Languages -- General; Computers -- Programming -- General; Mathematics -- Logic; Computers -- Intelligence (AI) & Semantics; Programming & scripting languages: general; Computer programming / software development; Mathematical theory of computation; Artificial intelligence; Software engineering; Logic design; Artificial intelligence; Computers -- Software Development & Engineering -- General; Software Engineering; Electronic books; Conference papers and proceedings
• Languages: English
• ISBNs: 9783319465203; 3319465201; 3319465198; 9783319465197
• Related ISBNs: 9783319465197
• Notes: Note: Online resource; title from PDF title page (SpringerLink, viewed October 13, 2016).
• Access Rights: Legal Deposit; Only available on premises controlled by the deposit library and to one user at any one time; The Legal Deposit Libraries (Non-Print Works) Regulations (UK).
• Access Usage: Restricted: Printing from this resource is governed by The Legal Deposit Libraries (Non-Print Works) Regulations (UK) and UK copyright law currently in force.