Automated Technology for Verification and Analysis: 9th International Symposium, ATVA 2011, Taipei, Taiwan, October 11-14, 2011. Proceedings

Front Matter....Pages -
Statistical Model Checking for Cyber-Physical Systems....Pages 1-12
Max and Sum Semantics for Alternating Weighted Automata....Pages 13-27
Making Software Verification Tools Really Work....Pages 28-42
Synthesizing, Verifying, and Debugging SoC with FSM-Based Specification of On-Chip Communication Protocols....Pages 43-50
Automated Analysis of Industrial Embedded Software....Pages 51-59
Nondeterministic Update of CTL Models by Preserving Satisfaction through Protections....Pages 60-74
Type-Based Automated Verification of Authenticity in Asymmetric Cryptographic Protocols....Pages 75-89
Formalization of Finite-State Discrete-Time Markov Chains in HOL....Pages 90-104
An Alternative Definition for Timed Automata Composition....Pages 105-119
Model Checking EGF on Basic Parallel Processes....Pages 120-134
Measuring Permissiveness in Parity Games: Mean-Payoff Parity Games Revisited....Pages 135-149
Algorithms for Synthesizing Priorities in Component-Based Systems....Pages 150-167
Trust Metrics for the SPKI/SDSI Authorisation Framework....Pages 168-182
Antichain-Based QBF Solving....Pages 183-197
A Hierarchical Approach for the Synthesis of Stabilizing Controllers for Hybrid Systems....Pages 198-212
Formal Analysis of Online Algorithms....Pages 213-227
Modal Transition Systems: Composition and LTL Model Checking....Pages 228-242
Efficient Inclusion Checking on Explicit and Semi-symbolic Tree Automata....Pages 243-258
Assembling Sessions....Pages 259-274
Parametric Modal Transition Systems....Pages 275-289
Policy Iteration within Logico-Numerical Abstract Domains....Pages 290-305
Small Strategies for Safety Games....Pages 306-320
Multi-core Nested Depth-First Search....Pages 321-335
Self-Loop Aggregation Product — A New Hybrid Approach to On-the-Fly LTL Model Checking....Pages 336-350
A Lightweight Approach for Loop Summarization....Pages 351-365
A Succinct Canonical Register Automaton Model....Pages 366-380
Parallel Nested Depth-First Searches for LTL Model Checking....Pages 381-396
Evaluating LTL Satisfiability Solvers....Pages 397-413
McAiT – A Timing Analyzer for Multicore Real-Time Software....Pages 414-417
MIO Workbench: A Tool for Compositional Design with Modal Input/Output Interfaces....Pages 418-421
The Buck Stops Here: Order, Chance, and Coordination in Distributed Control....Pages 422-431
Symbolic Verification and Test Generation for a Network of Communicating FSMs....Pages 432-442
Hierarchical Counterexamples for Discrete-Time Markov Chains....Pages 443-452
Efficient Loop Navigation for Symbolic Execution....Pages 453-462
An Efficient Algorithm for Learning Event-Recording Automata....Pages 463-472
Discretizing Affine Hybrid Automata with Uncertainty....Pages 473-481
What’s Decidable about Weighted Automata?....Pages 482-491
Widening with Thresholds for Programs with Complex Control Graphs....Pages 492-502
Linear Hybrid System Falsification through Local Search....Pages 503-510
Learning-Based Compositional Verification for Synchronous Probabilistic Systems....Pages 511-521
An Algorithmic Framework for Synthesis of Concurrent Programs....Pages 522-530
Back Matter....Pages -