Automated Technology for Verification and Analysis: 11th International Symposium, ATVA 2013, Hanoi, Vietnam, October 15-18, 2013. Proceedings

Front Matter....Pages -
Acceleration for Petri Nets....Pages 1-4
Automated Verification and Strategy Synthesis for Probabilistic Systems....Pages 5-22
SMT-Based Software Model Checking....Pages 23-23
Effective Translation of LTL to Deterministic Rabin Automata: Beyond the (F,G)-Fragment....Pages 24-39
Improved Upper and Lower Bounds for Büchi Disambiguation....Pages 40-54
Time-Bounded Reachability for Monotonic Hybrid Automata: Complexity and Fixed Points....Pages 55-70
An Automatic Technique for Checking the Simulation of Timed Systems....Pages 71-86
Synthesis of Bounded Integer Parameters for Parametric Timed Reachability Games....Pages 87-101
Kleene Algebras and Semimodules for Energy Problems....Pages 102-117
Looking at Mean-Payoff and Total-Payoff through Windows....Pages 118-132
Weighted Safety....Pages 133-147
A Framework for Ranking Vacuity Results....Pages 148-162
Synthesizing Masking Fault-Tolerant Systems from Deontic Specifications....Pages 163-177
Verification of a Dynamic Management Protocol for Cloud Applications....Pages 178-192
Compact Symbolic Execution....Pages 193-207
Multi-threaded Explicit State Space Exploration with State Reconstruction....Pages 208-223
Verification of Heap Manipulating Programs with Ordered Data by Extended Forest Automata....Pages 224-239
Integrating Policy Iterations in Abstract Interpreters....Pages 240-254
Interpolation Properties and SAT-Based Model Checking....Pages 255-271
Analysis of Message Passing Programs Using SMT-Solvers....Pages 272-286
An Expressive Framework for Verifying Deadlock Freedom....Pages 287-302
Expected Termination Time in BPA Games....Pages 303-318
Precise Cost Analysis via Local Reasoning....Pages 319-333
Control Flow Refinement and Symbolic Computation of Average Case Bound....Pages 334-348
Termination and Cost Analysis of Loops with Concurrent Interleavings....Pages 349-364
Linear Ranking for Linear Lasso Programs....Pages 365-380
Merge and Conquer: State Merging in Parametric Timed Automata....Pages 381-396
An Automata-Theoretic Approach to Reasoning about Parameterized Systems and Specifications....Pages 397-411
Pushdown Systems with Stack Manipulation....Pages 412-426
Robustness Analysis of String Transducers....Pages 427-441
Manipulating LTL Formulas Using Spot 1.0....Pages 442-445
Rabinizer 2: Small Deterministic Automata for LTL  ∖ GU ....Pages 446-450
LTL Model Checking with Neco....Pages 451-454
Solving Parity Games on the GPU....Pages 455-459
 PyEcdar : Towards Open Source Implementation for Timed Systems....Pages 460-463
 CCMC : A Conditional CSL Model Checker for Continuous-Time Markov Chains....Pages 464-468
NLTOOLBOX: A Library for Reachability Computation of Nonlinear Dynamical Systems....Pages 469-473
CELL: A Compositional Verification Framework....Pages 474-477
VCS: A Verifier for Component-Based Systems....Pages 478-481
SmacC: A Retargetable Symbolic Execution Engine....Pages 482-486
MoTraS: A Tool for Modal Transition Systems and Their Extensions....Pages 487-491
Cunf: A Tool for Unfolding and Verifying Petri Nets with Read Arcs....Pages 492-495
SAT Based Verification of Network Data Planes....Pages 496-505
A Theory for Control-Flow Graph Exploration....Pages 506-515
The Quest for Precision: A Layered Approach for Data Race Detection in Static Analysis....Pages 516-525
Back Matter....Pages -