Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques

Techniques.- Information flow analysis for Go.- Challenges in High-Assurance Runtime Verification .- Static versus Dynamic Verification in Why3, Frama-C and SPARK 2014.- Considering Type-State Verification for Quantified Event Automata.- Combining Static and Runtime Methods to Achieve Safe Standing-Up for Humanoid Robots.- On Combinations of Static and Dynamic Analysis.- Safer Refactorings.- Rigorous Engineering of Collective Adaptive Systems.- Programming of CAS systems by relying on attribute-based communication.- Towards Static Analysis of Policy-Based Self-Adaptive Computing Systems.- A Calculus for Open Ensembles and Their Composition.- Logic Fragments: coordinating entities with logic programs.- Mixed-Critical Systems Design with Coarse-grained Multi-core Interference.- A Library and Scripting Language for Tool Independent Simulation Descriptions.- Adaptation to the unforeseen: Do we master our autonomous systems?'-- Questions to the Panel.- Smart coordination of autonomic component ensembles in the context of ad-hoc communication.- A Tool-chain for Statistical Spatio-Temporal Model Checking of Bike-sharing Systems.- Rigorous graphical modelling of movement in Collective Adaptive Systems.- Integration and Promotion of Autonomy with the ARE Framework.- Safe Artificial Intelligence and Formal Methods.- Engineering Adaptivity, Universal Autonomous Systems, Ethics and Compliance Issues.- Correctness-by-Construction and Post-hoc Verification: Friends or Foes?.- Correctness-by-Construction and Post-hoc Verification: A Marriage of Convenience?.- Deductive Verification of Legacy Code.- Correctness-by-Construction $land$ Taxonomies $Rightarrow$\ Deep Comprehension of Algorithm Families.- Conditions for Compatibility of Components - The case of masters and slaves.- A Logic for Statistical Model Checking of Dynamic Software Architectures.- On two Friends  for getting Correct Programs - Automatically Translating Event-B Specifications to Recursive Algorithmsin Rodin.- Proof-Carrying Apps: Contract-Based Deployment-Time Verification.- Supervisory Controller Synthesis for Product Lines with CIF3.- Partial Verification and Intermediate Results as a Solution to Combine Automatic and Interactive Verification Techniques.- Security and Privacy of Protocols and Software with Formal Methods.- A Model-Based Approach to Secure Multiparty Distributed Systems.- Information leakage analysis of complex C code and its application to OpenSSL.- Integrated Modeling Workflow for Security Assurance.- A Privacy-Aware Conceptual Model for Handling Personal Data.- Guaranteeing Privacy-observing Data Exchange.