| Keynote Talks | |
| Program Verification Through Computer Algebra | p. 1 |
| JML's Rich, Inherited Specifications for Behavioral Subtypes | p. 2 |
| Three Perspectives in Formal Engineering | p. 35 |
| Specification and Verification | |
| A Method for Formalizing, Analyzing, and Verifying Secure User Interfaces | p. 55 |
| Applying Timed Interval Calculus to Simulink Diagrams | p. 74 |
| Reducing Model Checking of the Few to the One | p. 94 |
| Induction-Guided Falsification | p. 114 |
| Verifying [chi] Models of Industrial Systems with Spin | p. 132 |
| Stateful Dynamic Partial-Order Reduction | p. 149 |
| Internetware and Web-Based Systems | |
| User-Defined Atomicity Constraint: A More Flexible Transaction Model for Reliable Service Composition | p. 168 |
| Environment Ontology-Based Capability Specification for Web Service Discovery | p. 185 |
| Scenario-Based Component Behavior Derivation | p. 206 |
| Verification of Computation Orchestration Via Timed Automata | p. 226 |
| Towards the Semantics for Web Service Choreography Description Language | p. 246 |
| Type Checking Choreography Description Language | p. 264 |
| Concurrent, Communicating, Timing and Probabilistic Systems | |
| Formalising Progress Properties of Non-blocking Programs | p. 284 |
| Towards a Fully Generic Theory of Data | p. 304 |
| Verifying Statemate Statecharts Using CSP and FDR | p. 324 |
| A Reasoning Method for Timed CSP Based on Constraint Solving | p. 342 |
| Mapping RT-LOTOS Specifications into Time Petri Nets | p. 360 |
| Reasoning Algebraically About Probabilistic Loops | p. 380 |
| Object and Component Orientation | |
| Formal Verification of the Heap Manager of an Operating System Using Separation Logic | p. 400 |
| A Statically Verifiable Programming Model for Concurrent Object-Oriented Programs | p. 420 |
| Model Checking Dynamic UML Consistency | p. 440 |
| Testing and Model Checking | |
| Conditions for Avoiding Controllability Problems in Distributed Testing | p. 460 |
| Generating Test Cases for Constraint Automata by Genetic Symbiosis Algorithm | p. 478 |
| Checking the Conformance of Java Classes Against Algebraic Specifications | p. 494 |
| Incremental Slicing | p. 514 |
| Assume-Guarantee Software Verification Based on Game Semantics | p. 529 |
| Optimized Execution of Deterministic Blocks in Java PathFinder | p. 549 |
| Tools | |
| A Tool for a Formal Pattern Modeling Language | p. 568 |
| An Open Extensible Tool Environment for Event-B | p. 588 |
| Tool for Translating Simulink Models into Input Language of a Model Checker | p. 606 |
| Fault-Tolerance and Security | |
| Verifying Abstract Information Flow Properties in Fault Tolerant Security Devices | p. 621 |
| A Language for Modeling Network Availability | p. 639 |
| Multi-process Systems Analysis Using Event B: Application to Group Communication Systems | p. 660 |
| Specification and Refinement | |
| Issues in Implementing a Model Checker for Z | p. 678 |
| Taking Our Own Medicine: Applying the Refinement Calculus to State-Rich Refinement Model Checking | p. 697 |
| Discovering Likely Method Specifications | p. 717 |
| Time Aware Modelling and Analysis of Multiclocked VLSI Systems | p. 737 |
| SALT-Structured Assertion Language for Temporal Logic | p. 757 |
| Author Index | p. 777 |
| Table of Contents provided by Ingram. All Rights Reserved. |