Automated Technology for Verification and Analysis: 8th International Symposium, ATVA 2010, Singapore, September 21-24, 2010. Proceedings

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 -