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.