Automated Technology for Verification and Analysis

Invited Papers.-Acceleration for Petri Nets.- Automated Verification and Strategy Synthesis for Probabilistic Systems.- SMT-Based Software Model Checking: Explicit Scheduler, Symbolic Threads.- Regular Papers.-Effective Translation of LTL to Deterministic Rabin Automata: Beyond the (F,G)-Fragment.- Improved Upper and Lower Bounds for Buchi Disambiguation.- Time-Bounded Reachability for Monotonic Hybrid Automata: Complexity and Fixed Points.- An Automatic Technique for Checking the Simulation of Timed Systems.- Synthesis of Bounded Integer Parameters for Parametric Timed Reachability Games.- Kleene Algebras and Semimodules for Energy Problems.- Looking at Mean-Payoff and Total-Payoff through Windows.- Weighted Safety.- A Framework for Ranking Vacuity Results.- Synthesizing Masking Fault-Tolerant Systems from Deontic Specifications.- Verification of a Dynamic Management Protocol for Cloud Applications.- Compact Symbolic Execution.- Multi-threaded Explicit State Space Exploration with State Reconstruction.- Verification of Heap Manipulating Programs with Ordered Data by Extended Forest Automata.- Integrating Policy Iterations in Abstract Interpreters.- Interpolation Properties and SAT-Based Model Checking.- Analysis of Message Passing Programs Using SMT-Solvers.- An Expressive Framework for Verifying Deadlock Freedom.- Expected Termination Time in BPA Games.- Precise Cost Analysis via Local Reasoning.- Control Flow Refinement and Symbolic Computation of Average Case Bound.- Termination and Cost Analysis of Loops with Concurrent Interleavings.- Linear Ranking for Linear Lasso Programs.- Merge and Conquer: State Merging in Parametric Timed Automata.- An Automata-Theoretic Approach to Reasoning about Parameterized Systems and Specifications.- Pushdown Systems with Stack Manipulation.- Robustness Analysis of String Transducers.- Tool Papers.- Manipulating LTL Formulas Using Spot 1.0.- Rabinizer 2: Small Deterministic Automata for LTLGU.- LTL Model Checking with Neco.- Solving Parity Games on the GPU.- PyEcdar: Towards Open Source Implementation for Timed Systems.- CCMC: A Conditional CSL Model Checker for Continuous-Time Markov Chains.- NLTOOLBOX: A Library for Reachability Computation of Nonlinear Dynamical Systems.- CELL: A Compositional Verification Framework.- VCS: A Verifier for Component-Based Systems.- SmacC: A Retargetable Symbolic Execution Engine.- MoTraS: A Tool for Modal Transition Systems and Their Extensions.- Cunf: A Tool for Unfolding and Verifying Petri Nets with Read Arcs.- Short Papers.- SAT Based Verification of Network Data Planes.- A Theory for Control-Flow Graph Exploration.- The Quest for Precision: A Layered Approach for Data Race Detection in Static Analysis.