Shape and Content: A Database-Theoretic Perspective on the Analysis of Data Structures -- How to Break the Bank: Semantics of Capability Policies -- Model-Checking Circus State-Rich Specifications -- An Interactive Verification Tool Meets an IDE -- An Analysis Pathway for the Quantitative Evaluation of Public Transport Systems -- Modeling UML Template Classes with FoCaLiZe -- Integrating Event-B Modelling and Discrete-Event Simulation to Analyse Resilience of Data Stores in the Cloud -- Applying an Integrated Modelling Process to Run-time Management of Many-Core Systems -- Verifying Behavioral UML Systems via CEGAR -- Formal Refinement in SysML -- Verifying Modal Workflow Specifications Using Constraint Solving.-Proofs and Refutations in Invariant-Based Programming -- Automated Theorem Prover Assisted Program Calculations -- Managing LTL Properties in Event-B Refinement -- Formal Security Analysis of the MaCAN Protocol -- A Probabilistic Framework for Security Scenarios with Dependent Actions -- A Hybrid Analysis for Security Protocols with State -- Towards a Formal Semantics-Based Technique for Interprocedural Slicing -- Integrating Software and Hardware Verification -- Code Generation for Event-B -- Verifying Linearizability on TSO Architectures -- A Compositional Proof Method for Linearizability Applied to a Wait-Free Multiset -- A Separation Principle for Embedded System Interfacing.