Automated Technology for Verification and Analysis

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!.