Automated Technology for Verification and Analysis: 9th International Symposium, ATVA 2011, Taipei, Taiwan, October 11-14, 2011, Proceedings (Lecture Notes in Computer Science (6996))

This book constitutes the refereed proceedings of the 9th International Symposium on Automated Technology for Verification and Analysis, ATVA 2011, held in Taipei, Taiwan, in October 2011. The 23 revised regular papers presented together with 5 invited papers, 11 short papers, and 2 tool papers, were carefully reviewed and selected from 75 submissions. The papers address all theoretical and practical aspects of automated analysis, verification and synthesis; thus providing a forum for interaction between the regional and the international research communities and industry in the field. 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 - Constitutes the refereed proceedings of the 9th International Symposium on Automated Technology for Verification and Analysis, ATVA 2011, held in Taipei, Taiwan, in October 2011. This book includes the papers addressing theoretical and practical aspects of automated analysis, verification and synthesis.