Automated Technology for Verification and Analysis: 8th International Symposium, ATVA 2010, Singapore, September 21-24, 2010, Proceedings (Lecture Notes in Computer Science (6252))

Annotation. This Book Constitutes The Refereed Proceedings Of The 8th International Symposium On Automated Technology For Verification And Analysis, Atva 2010, Held In Singapore, In September 2010. The Book Includes 3 Invited Talks, 21 Regular Papers And 9 Tool Papers. Front Matter....Pages - Probabilistic Automata on Infinite Words: Decidability and Undecidability Results....Pages 1-16 Abstraction Learning....Pages 17-17 Synthesis: Words and Traces....Pages 18-21 Promptness in ω -Regular Automata....Pages 22-36 Using Redundant Constraints for Refinement....Pages 37-51 Methods for Knowledge Based Controlling of Distributed Systems....Pages 52-66 Composing Reachability Analyses of Hybrid Systems for Safety and Stability....Pages 67-81 The Complexity of Codiagnosability for Discrete Event and Timed Systems....Pages 82-96 On Scenario Synchronization....Pages 97-111 Compositional Algorithms for LTL Synthesis....Pages 112-127 What’s Decidable about Sequences?....Pages 128-142 A Study of the Convergence of Steady State Probabilities in a Closed Fork-Join Network....Pages 143-157 Lattice-Valued Binary Decision Diagrams....Pages 158-172 A Specification Logic for Exceptions and Beyond....Pages 173-187 Non-monotonic Refinement of Control Abstraction for Concurrent Programs....Pages 188-202 An Approach for Class Testing from Class Contracts....Pages 203-217 Efficient On-the-Fly Emptiness Check for Timed Büchi Automata....Pages 218-232 Reachability as Derivability, Finite Countermodels and Verification....Pages 233-244 LTL Can Be More Succinct....Pages 245-258 Automatic Generation of History-Based Access Control from Information Flow Specification....Pages 259-275 Auxiliary Constructs for Proving Liveness in Compassion Discrete Systems....Pages 276-290 Symbolic Unfolding of Parametric Stopwatch Petri Nets....Pages 291-305 Recursive Timed Automata....Pages 306-324 Probabilistic Contracts for Component-Based Design....Pages 325-340 Model-Checking Web Applications with Web-TLR ....Pages 341-346 GAVS: Game Arena Visualization and Synthesis....Pages 347-352 CRI: Symboli c Debugge r for MCAP I Applications....Pages 353-358 MCGP: A Software Synthesis Tool Based on Model Checking and Genetic Programming....Pages 359-364 ECDAR: An Environment for Compositional Design and Analysis of Real Time Systems....Pages 365-370 Developing Model Checkers Using PAT....Pages 371-377 YAGA: Automated Analysis of Quantitative Safety Specifications in Probabilistic B....Pages 378-386 COMBINE: A Tool on Combined Formal Methods for Bindingly Verification....Pages 387-395 Rbminer: A Tool for Discovering Petri Nets from Transition Systems....Pages 396-402 Back Matter....Pages - A book that constitutes the refereed proceedings of the 8th International Symposium on Automated Technology for Verification and Analysis, ATVA 2010, that was held in Singapore, in September 2010. It includes 3 invited talks, 21 regular papers and 9 tool papers.