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, partial-order reductions; solving procedures, model checking; and program analysis.
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 SMT-Based Parameter
Synthesis with Application to Piecewise Multi-Affine Systems.- Complexity,
Decidability.- On Finite Domains in First-Order Linear Temporal Logic.-
Decidability Results for Multi-Objective Stochastic Games.- A Decision
Procedure for Separation Logic in SMT.- Solving Mean-Payoff Games on the
GPU.- Synthesis, Refinement.- Synthesizing Skeletons for Reactive Systems.-
Observational Refinement and Merge for Disjunctive MTSs.- Equivalence-Based
Abstraction Refinement for muHORS Model Checking.- Optimization, Heuristics,
Partial-Order Reductions.- Greener Bits: Formal Analysis of Demand Response.-
Heuristics for Checking Liveness Properties with Partial Order Reductions. -
Partial-Order 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 Cloud-Based SMT Solving.- Symbolic Model
Checking for Factored Probabilistic Models.- Program Analysis.- A
Sketching-Based Approach for Debugging Using Test Cases.- Polynomial
Invariants by Linear Algebra.- Certified Symbolic Execution.- Tighter Loop
Bound Analysis.
