Automated technology for verification and analysis : 14th International Symposium, ATVA 2016, Chiba, Japan, October 1720, 2016, Proceedings
 Responsibility
 Cyrille Artho, Axel Legay, Doron Peled (eds.).
 Digital
 text file
 Publication
 Cham, Switzerland : Springer, 2016.
 Physical description
 1 online resource (xi, 530 pages) : illustrations
 Series
 Lecture notes in computer science ; 9938. 03029743
 LNCS sublibrary. SL 2, Programming and software engineering.
Online
More options
Description
Creators/Contributors
 Meeting
 ATVA (Symposium) (14th : 2016 : Chiba, Japan)
 Contributor
 Artho, Cyrille, editor.
 Legay, Axel, editor.
 Peled, Doron A., 1962 editor.
Contents/Summary
 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 StateSpace 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 PSPACEcomplete; 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 CommandLine Tools; 3 The Python Interface; 4 Model Checkers Built Using Spot; References; MoChiBA: Probabilistic LTL Model Checking Using LimitDeterministic Büchi Automata; 1 Introduction; 2 Overview of the Algorithm
 Keynote
 Synthesizing and Completely Testing Hardware based on Templates through Small Numbers of Test Patterns
 Markov Models, Chains, and Decision Processes
 Approximate Policy Iteration for Markov Decision Processes via Quantitative Adaptive Aggregations. Optimizing the Expected Mean Payoff in Energy Markov Decision Processes
 Parameter Synthesis for Markov Models: Faster Than Ever
 Bounded Model Checking for Probabilistic Programs
 Counter Systems, Automata
 How Hard Is It to Verify Flat Affine Counter Systems with the Finite Monoid Property
 Solving Language Equations using Flanked Automata
 Spot 2.0
 a Framework for LTL and ωAutomata Manipulation
 MoChiBA: Probabilistic LTL Model Checking Using Limit Deterministic Büchi Automata
 Parallelism, Concurrency
 Synchronous Products of Rewrite Systems
 Specifying and Verifying Secrecy in Workflows with Arbitrarily Many Agents
 Lazy Sequentialization for the Safety Verification of Unbounded Concurrent Programs
 Parallel SMTBased Parameter Synthesis with Application to Piecewise MultiAffine Systems
 Complexity, Decidability
 On Finite Domains in FirstOrder Linear Temporal Logic
 Decidability Results for MultiObjective Stochastic Games
 A Decision Procedure for Separation Logic in SMT
 Solving MeanPayoff Games on the GPU
 Synthesis, Refinement
 Synthesizing Skeletons for Reactive Systems
 Observational Refinement and Merge for Disjunctive MTSs
 EquivalenceBased Abstraction Refinement for muHORS Model Checking
 Optimization, Heuristics, PartialOrder Reductions
 Greener Bits: Formal Analysis of Demand Response
 Heuristics for Checking Liveness Properties with Partial Order Reductions.
 PartialOrder Reduction for GPU Model Checking
 Efficient Verification of Program Fragments: Eager POR
 Solving Procedures, Model Checking
 Skolem Functions for DQBF
 STL Model Checking of Continuous and Hybrid Systems
 Clause Sharing and Partitioning for CloudBased SMT Solving
 Symbolic Model Checking for Factored Probabilistic Models
 Program Analysis
 A SketchingBased Approach for Debugging Using Test Cases
 Polynomial Invariants by Linear Algebra
 Certified Symbolic Execution
 Tighter Loop Bound Analysis.
 Summary
 This book constitutes the proceedings of the 14th International Symposium on Automated Technology for Verification and Analysis, ATVA 2016, held in Chiba, Japan, in October 2016. The 31 papers presented in this volume were carefully reviewed and selected from 82 submissions. They were organized in topical sections named: keynote; Markov models, chains, and decision processes; counter systems, automata; parallelism, concurrency; complexity, decidability; synthesis, refinement; optimization, heuristics, partialorder reductions; solving procedures, model checking; and program analysis.
Subjects
 Subjects
 Automatic theorem proving > Congresses.
 Artificial intelligence > Congresses.
 Computer Science.
 Software Engineering.
 Programming Languages, Compilers, Interpreters.
 Logics and Meanings of Programs.
 Mathematical Logic and Formal Languages.
 Artificial Intelligence (incl. Robotics)
 Programming Techniques.
 Programming & scripting languages: general.
 Computer programming > software development.
 Mathematical theory of computation.
 Artificial intelligence.
 Computers > Programming Languages > General.
 Computers > Programming > General.
 Mathematics > Logic.
 Computers > Intelligence (AI) & Semantics.
 Computers > Software Development & Engineering > General.
 Automatic theorem proving.
Bibliographic information
 Publication date
 2016
 Title variation
 ATVA 2016
 Series
 Lecture notes in computer science, 03029743 ; 9938
 LNCS sublibrary. SL 2, Programming and software engineering
 Note
 International conference proceedings.
 Includes author index.
 ISBN
 9783319465203 (electronic bk.)
 3319465201 (electronic bk.)
 3319465198
 9783319465197
 9783319465197 (print)
 DOI
 10.1007/9783319465203