§16§This book constitutes the refereed proceedings of the 11th International Symposium on Automated Technology for Verification and Analysis, ATVA 2013, held at Hanoi, Vietnam, in October 2013.The 27 regular papers, 3 short papers and 12 tool papers presented together with 3 invited talks were carefully selected from73 submissions.The papers are organized in topical, sections on analysis and verification of hardware circuits, systems-on-chip and embedded systems, analysis of real-time, hybrid, priced/weighted and probabilistic systems, deductive, algorithmic, compositional, and abstraction/refinement techniques for analysis and verification, analytical techniques for safety, security, and dependability, testing and runtime analysis based on verification technology, analysis and verification of parallel and concurrent hardware/software systems, verification in industrial practice, and applications and case studies. §04§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 wi §04§th 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 §04§ 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.
