Alloy: A Logical Modelling Language -- An Outline Pattern Language for Z: Five Illustrations and Two Tables -- Patterns to Guide Practical Refactoring: Examples Targetting Promotion in Z -- Reuse of Specification Patterns with the B Method -- Composing Specifications Using Communication -- When Concurrent Control Meets Functional Requirements, or Z + Petri-Nets -- How to Diagnose a Modern Car with a Formal B Model? -- Parallel Hardware Design in B -- Operation Refinement and Monotonicity in the Schema Calculus -- Using Coupled Simulations in Non-atomic Refinement -- An Analysis of Forward Simulation Data Refinement -- B#: Toward a Synthesis between Z and B -- Introducing Backward Refinement into B -- Expression Transformers in B-GSL -- Probabilistic Termination in B -- Probabilistic Invariants for Probabilistic Machines -- Proving Temporal Properties of Z Specifications Using Abstraction -- Compositional Verification for Object-Z -- Timed CSP and Object-Z -- Object Orientation without Extending Z -- Comparison of Formalisation Approaches of UML Class Constructs in Z and Object-Z -- Towards Practical Proofs of Class Correctness -- Automatically Generating Information from a Z Specification to Support the Classification Tree Method -- Refinement Preserves PLTL Properties -- Proving Event Ordering Properties for Information Systems -- ZML: XML Support for Standard Z -- Formal Derivation of Spanning Trees Algorithms -- Using B Refinement to Analyse Compensating Business Processes -- A Formal Specification in B of a Medical Decision Support System -- Extending B with Control Flow Breaks -- Towards Dynamic Population Management of Abstract Machines in the B Method.