Automated Technology for Verification and Analysis Third International Symposium, ATVA 2005, Taipei, Taiwan, October 4-7, 2005. Proceedings /
The Automated Technology for Veri?cation and Analysis (ATVA) international symposium series was initiated in 2003, responding to a growing interest in formal veri?cation spurred by the booming IT industry, particularly hardware design and manufacturing in East Asia. Its purpose is to promote researc...
| Συγγραφή απο Οργανισμό/Αρχή: | |
|---|---|
| Άλλοι συγγραφείς: | , |
| Μορφή: | Ηλεκτρονική πηγή Ηλ. βιβλίο |
| Γλώσσα: | English |
| Έκδοση: |
Berlin, Heidelberg :
Springer Berlin Heidelberg,
2005.
|
| Σειρά: | Lecture Notes in Computer Science,
3707 |
| Θέματα: | |
| Διαθέσιμο Online: | Full Text via HEAL-Link |
Πίνακας περιεχομένων:
- Keynote Speeches
- Ranking Abstraction as a Companion to Predicate Abstraction
- Termination and Invariance Analysis of Loops
- Some Perspectives of Infinite-State Verification
- Model Checking
- Verifying Very Large Industrial Circuits Using 100 Processes and Beyond
- A New Reachability Algorithm for Symmetric Multi-processor Architecture
- Comprehensive Verification Framework for Dependability of Self-optimizing Systems
- Exploiting Hub States in Automatic Verification
- Combined Methods
- An Approach for the Verification of SystemC Designs Using AsmL
- Decomposition-Based Verification of Cyclic Workflows
- Timed, Embedded, and Hybrid Systems (I)
- Guaranteed Termination in the Verification of LTL Properties of Non-linear Robust Discrete Time Hybrid Systems
- Computation Platform for Automatic Analysis of Embedded Software Systems Using Model Based Approach
- Quantitative and Qualitative Analysis of Temporal Aspects of Complex Activities
- Automatic Test Case Generation with Region-Related Coverage Annotations for Real-Time Systems
- Abstraction and Reduction Techniques
- Selective Search in Bounded Model Checking of Reachability Properties
- Predicate Abstraction of RTL Verilog Descriptions Using Constraint Logic Programming
- State Space Exploration of Object-Based Systems Using Equivalence Reduction and the Sweepline Method
- Syntactical Colored Petri Nets Reductions
- Decidability and Complexity
- Algorithmic Algebraic Model Checking II: Decidability of Semi-algebraic Model Checking and Its Applications to Systems Biology
- A Static Analysis Using Tree Automata for XML Access Control
- Reasoning About Transfinite Sequences
- Semi-automatic Distributed Synthesis
- Established Formalisms and Standards
- A New Graph of Classes for the Preservation of Quantitative Temporal Constraints
- Comparison of Different Semantics for Time Petri Nets
- Introducing Dynamic Properties with Past Temporal Operators in the B Refinement
- Approximate Reachability for Dead Code Elimination in Esterel???
- Compositional Verification and Games
- Synthesis of Interface Automata
- Multi-valued Model Checking Games
- Timed, Embedded, and Hybrid Systems (II)
- Model Checking Prioritized Timed Automata
- An MTBDD-Based Implementation of Forward Reachability for Probabilistic Timed Automata
- Protocols Analysis, Case Studies, and Tools
- An EFSM-Based Intrusion Detection System for Ad Hoc Networks
- Modeling and Verification of a Telecommunication Application Using Live Sequence Charts and the Play-Engine Tool
- Formal Construction and Verification of Home Service Robots: A Case Study
- Model Checking Real Time Java Using Java PathFinder
- Infinite-State and Parameterized Systems
- Using Parametric Automata for the Verification of the Stop-and-Wait Class of Protocols
- Flat Acceleration in Symbolic Model Checking
- Flat Counter Automata Almost Everywhere!.
