KEYNOTE SPEECHES.- Ranking Abstraction as Companion to Predicate Abstraction.- Developing High Quality Software with Formal Methods: What Else Is Needed?.- A Testing Architecture for Designing High-Reliable MANET Protocols.- REGULAR PAPERS.- A Composition Operator for Systems with Active and Passive Actions.- A Formal Semantics of UML StateCharts by Means of Timed Petri Nets.- A Hierarchy of Implementable MSC Languages.- Combining Static Analysis and Model Checking for Systems Employing Commutative Functions.- Fast Generic Model-Checking for Data-Based Systems.- Logic and Model Checking for Hidden Markov Models.- Proving ??-Calculus Properties with SAT-Based Model Checking.- Ad Hoc Routing Protocol Verification Through Broadcast Abstraction.- Discovering Chatter and Incompleteness in the Datagram Congestion Control Protocol.- Thread Allocation Protocols for Distributed Real-Time and Embedded Systems.- A Petri Net View of Mobility.- Modular Verification of Petri Nets Properties: A Structure-Based Approach.- An Improved Conformance Testing Method.- Resolving Observability Problems in Distributed Test Architectures.- Automatic Generation of Conflict-Free IPsec Policies.- A Framework Based Approach for Formal Modeling and Analysis of Multi-level Attacks in Computer Networks.- Model Checking for Timed Statecharts.- Abstraction-Guided Model Checking Using Symbolic IDA* and Heuristic Synthesis.- Modeling and Verification of Safety-Critical Systems Using Safecharts.- Structure Preserving Data Abstractions for Statecharts.- Amortised Bisimulations.- Proof Methodologies for Behavioural Equivalence in Dpi.- Deriving Non-determinism from Conjunction and Disjunction.- Abstract Operational Semantics for Use Case Maps.- ArchiTRIO: A UML-Compatible Language for ArchitecturalDescription and Its Formal Semantics.- Submodule Construction for Extended State Machine Models.- Towards Synchronizing Linear Collaborative Objects with Operational Transformation.- Designing Efficient Fail-Safe Multitolerant Systems.- Hierarchical Decision Diagrams to Exploit Model Structure.- Computing Subgraph Probability of Random Geometric Graphs: Quantitative Analyses of Wireless Ad Hoc Networks.- Formalising Web Services.- From Automata Networks to HMSCs: A Reverse Model Engineering Perspective.- Properties as Processes: Their Specification and Verification.- SHORT PAPERS.- Epoch Distance of the Random Waypoint Model in Mobile Ad Hoc Networks.- Automatic Partitioner for Behavior Level Distributed Logic Simulation.- Expressive Completeness of an Event-Pattern Reactive Programming Language.- Formalizing Interoperability Testing: Quiescence Management and Test Generation.- Formal Description of Mobile IPv6 Protocol.- Incremental Modeling Under Large-Scale Distributed Interaction.- The Inductive Approach to Strand Space.- Compositional Modelling and Verification of IPv6 Mobility.
