Automated Technology for Verification and Analysis [electronic resource] : 11th International Symposium, ATVA 2013, Hanoi, Vietnam, October 15-18, 2013. Proceedings / edited by Dang Van Hung, Mizuhito Ogawa.

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 B¨uchi 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 LTL\GU -- 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.