Automated Technology for Verification and Analysis: Third International Symposium, ATVA 2005, Taipei, Taiwan, October 4-7, 2005. Proceedings

Front Matter....Pages -
Ranking Abstraction as a Companion to Predicate Abstraction....Pages 1-1
Termination and Invariance Analysis of Loops....Pages 2-2
Some Perspectives of Infinite-State Verification....Pages 3-10
Verifying Very Large Industrial Circuits Using 100 Processes and Beyond....Pages 11-25
A New Reachability Algorithm for Symmetric Multi-processor Architecture....Pages 26-38
Comprehensive Verification Framework for Dependability of Self-optimizing Systems....Pages 39-53
Exploiting Hub States in Automatic Verification....Pages 54-68
An Approach for the Verification of SystemC Designs Using AsmL....Pages 69-83
Decomposition-Based Verification of Cyclic Workflows....Pages 84-98
Guaranteed Termination in the Verification of LTL Properties of Non-linear Robust Discrete Time Hybrid Systems....Pages 99-113
Computation Platform for Automatic Analysis of Embedded Software Systems Using Model Based Approach....Pages 114-128
Quantitative and Qualitative Analysis of Temporal Aspects of Complex Activities....Pages 129-143
Automatic Test Case Generation with Region-Related Coverage Annotations for Real-Time Systems....Pages 144-158
Selective Search in Bounded Model Checking of Reachability Properties....Pages 159-173
Predicate Abstraction of RTL Verilog Descriptions Using Constraint Logic Programming....Pages 174-186
State Space Exploration of Object-Based Systems Using Equivalence Reduction and the Sweepline Method....Pages 187-201
Syntactical Colored Petri Nets Reductions....Pages 202-216
Algorithmic Algebraic Model Checking II: Decidability of Semi-algebraic Model Checking and Its Applications to Systems Biology....Pages 217-233
A Static Analysis Using Tree Automata for XML Access Control....Pages 234-247
Reasoning About Transfinite Sequences....Pages 248-262
Semi-automatic Distributed Synthesis....Pages 263-277
A New Graph of Classes for the Preservation of Quantitative Temporal Constraints....Pages 278-292
Comparison of Different Semantics for Time Petri Nets....Pages 293-307
Introducing Dynamic Properties with Past Temporal Operators in the B Refinement....Pages 308-322
Approximate Reachability for Dead Code Elimination in Esterel  ⋆  ....Pages 323-337
Synthesis of Interface Automata....Pages 338-353
Multi-valued Model Checking Games....Pages 354-369
Model Checking Prioritized Timed Automata....Pages 370-384
An MTBDD-Based Implementation of Forward Reachability for Probabilistic Timed Automata....Pages 385-399
An EFSM-Based Intrusion Detection System for Ad Hoc Networks....Pages 400-413
Modeling and Verification of a Telecommunication Application Using Live Sequence Charts and the Play-Engine Tool....Pages 414-428
Formal Construction and Verification of Home Service Robots: A Case Study....Pages 429-443
Model Checking Real Time Java Using Java PathFinder....Pages 444-456
Using Parametric Automata for the Verification of the Stop-and-Wait Class of Protocols....Pages 457-473
Flat Acceleration in Symbolic Model Checking....Pages 474-488
Flat Counter Automata Almost Everywhere!....Pages 489-503
Back Matter....Pages -