E-raamat: Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques: 7th International Symposium, ISoLA 2016, Imperial, Corfu, Greece, October 10-14, 2016, Proceedings, Part I

Statistical Model Checking: Past, Present and Future.- Hypothesis
testing for rare-event simulation: limitations and possibilities.- Survey of
Statistical Verification of Linear Unbounded Properties: Model Checking and
Distances.- Feedback Control for Statistical Model Checking of Cyber-Physical
Systems.- Probabilistic Model Checking of Incomplete Models.- Plasma Lab: A
Modular Statistical Model Checking Platform.- Synthesizing Energy-Optimal
Controllers for Multiprocessor Dataflow Applications with UPPAAL STRATEGO.-
Statistical Model Checking for Product Lines.- Towards Adaptive Scheduling of
Maintenance for Cyber-Physical Systems.- Better railway engineering through
statistical model checking.- On Creation and Analysis of Reliability Models
by Means of Stochastic Timed Automata and Statistical Model Checking:
Principle.-  Automatic Synthesis of Code using Genetic Programming.-
Evaluation and Reproducibility of Program Analysis and Verification (Track
Introduction).- Symbolic Execution with CEGAR.- Multi-Core Model Checking of
Large-Scale Reactive Systems Using Different State Representations.- Sparse
Analysis of Variable Path Predicates Based Upon SSA-Form.- A Model
Interpreter for Timed Automata.- ModSyn-PP: Modular Synthesis of Programs and
Processes: Track Introduction.- Combinatory Process Synthesis.- Synthesis
from a Practical Perspective.- A Long and Winding Road Towards Modular
Synthesis.- Semantic heterogeneity in the formal development of complex
systems: an introduction.- On the Use of Domain and System Knowledge Modeling
in Goal-Based Event-B Specifications.- Strengthening MDE and Formal Design
Models by references to Domain Ontologies. A Model Annotation Based
Approach.- Towards Functional Requirements Analytics.- Heterogeneous
Semantics and Unifying Theories.- Static and Runtime Verification:
Competitors or Friends?.- StaRVOOrS - Episode II, Strengthen and Distribute
the Force.- A Model-Based Approach to Combining Static and Dynamic
Verification 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.