Integrated Formal Methods

Invited Talks.- SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft.- Design Verification for Control Engineering.- Integrating Model Checking and Theorem Proving in a Reflective Functional Language.- Tutorial.- A Tutorial Introduction to Designs in Unifying Theories of Programming.- Contributed Papers.- An Integration of Program Analysis and Automated Theorem Proving.- Verifying Controlled Components.- Efficient CSP Z Data Abstraction.- State/Event-Based Software Model Checking.- Formalising Behaviour Trees with CSP.- Generating MSCs from an Integrated Formal Specification Language.- UML to B: Formal Verification of Object-Oriented Models.- Software Verification with Integrated Data Type Refinement for Integer Arithmetic.- Constituent Elements of a Correctness-Preserving UML Design Approach.- Relating Data Independent Trace Checks in CSP with UNITY Reachability under a Normality Assumption.- Linking CSP-OZ with UML and Java: A Case Study.- Object-Oriented Modelling with High-Level Modular Petri Nets.- Specification and Verification of Synchronizing Concurrent Objects.- Understanding Object-Z Operations as Generalised Substitutions.- Embeddings of Hybrid Automata in Process Algebra.- An Optimal Approach to Hardware/Software Partitioning for Synchronous Model.- A Many-Valued Logic with Imperative Semantics for Incremental Specification of Timed Models.- Integrating Temporal Logics.- Integration of Specification Languages Using Viewpoints.- Integrating Formal Methods by Unifying Abstractions.- Formally Justifying User-Centred Design Rules: A Case Study on Post-completion Errors.- Using UML Sequence Diagrams as the Basis for a Formal Test Description Language.- Viewpoint-Based Testing of Concurrent Components.- A Method for Compiling and Executing Expressive Assertions.