Using Design Patterns in Formal Methods: An Event-B Approach -- A Unified Approach to Abstract Interpretation, Formal Verification and Testing of C/C++ Modules -- The Three Platonic Models of Divergence-Strict CSP -- Monotonic Abstraction in Action -- Non-interleaving Semantics with Causality for Nondeterministic Dataflow -- Symbolic Reachability for Process Algebras with Recursive Data Types -- Inclusion Test Algorithms for One-Unambiguous Regular Expressions -- Refinement of Kripke Models for Dynamics -- Tomorrow and All our Yesterdays: MTL Satisfiability over the Integers -- A Theory of Pointers for the UTP -- Recasting Constraint Automata into Büchi Automata -- A Complete Realisability Semantics for Intersection Types and Arbitrary Expansion Variables -- Towards Efficient Verification of Systems with Dynamic Process Creation -- An Observational Model for Transactional Calculus of Services Orchestration -- Everything Is PSPACE-Complete in Interaction Systems -- A New Approach for the Construction of Multiway Decision Graphs -- Congruence Results of Scope Equivalence for a Graph Rewriting Model of Concurrent Programs -- Guided Test Generation from CSP Models -- Relaxing Goodness Is Still Good -- Benchmarking Model- and Satisfiability-Checking on Bi-infinite Time -- Formal Analysis of Workflows Using UML 2.0 Activities and Graph Transformation Systems -- Testing Concurrent Objects with Application-Specific Schedulers -- A Theory of Bounded Fair Scheduling -- Fair Exchange Is Incomparable to Consensus -- Automatic Generation of CSP