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.
Author(s): Krishnendu Chatterjee, Thomas A. Henzinger (auth.), Ahmed Bouajjani, Wei-Ngan Chin (eds.)
Series: Lecture Notes in Computer Science 6252 : Programming and Software Engineering
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 2010
Language: English
Pages: 404
Tags: Software Engineering; Programming Techniques; Computer Communication Networks; Logics and Meanings of Programs; Programming Languages, Compilers, Interpreters; Software Engineering/Programming and Operating Systems
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 -
