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

Front Matter....Pages I-XXIII
Front Matter....Pages 1-1
Statistical Model Checking: Past, Present, and Future....Pages 3-15
Hypothesis Testing for Rare-Event Simulation: Limitations and Possibilities....Pages 16-26
Survey of Statistical Verification of Linear Unbounded Properties: Model Checking and Distances....Pages 27-45
Feedback Control for Statistical Model Checking of Cyber-Physical Systems....Pages 46-61
Probabilistic Model Checking of Incomplete Models....Pages 62-76
Plasma Lab: A Modular Statistical Model Checking Platform....Pages 77-93
Statistical Model Checking for Product Lines....Pages 94-113
Towards Adaptive Scheduling of Maintenance for Cyber-Physical Systems....Pages 114-133
Better Railway Engineering Through Statistical Model Checking....Pages 134-150
On Creation and Analysis of Reliability Models by Means of Stochastic Timed Automata and Statistical Model Checking: Principle....Pages 151-165
Automatic Synthesis of Code Using Genetic Programming....Pages 166-181
Front Matter....Pages 182-187
Evaluation and Reproducibility of Program Analysis and Verification (Track Introduction)....Pages 189-189
Symbolic Execution with CEGAR....Pages 191-194
Multi-core Model Checking of Large-Scale Reactive Systems Using Different State Representations....Pages 195-211
Sparse Analysis of Variable Path Predicates Based upon SSA-Form....Pages 212-226
A Model Interpreter for Timed Automata....Pages 227-242
Front Matter....Pages 243-258
ModSyn-PP: Modular Synthesis of Programs and Processes Track Introduction....Pages 259-259
Combinatory Process Synthesis....Pages 261-265
Synthesis from a Practical Perspective....Pages 266-281
Front Matter....Pages 282-302
A Long and Winding Road Towards Modular Synthesis....Pages 259-259
Front Matter....Pages 303-317
Semantic Heterogeneity in the Formal Development of Complex Systems: An Introduction....Pages 319-319
On the Use of Domain and System Knowledge Modeling in Goal-Based Event-B Specifications....Pages 321-324
Strengthening MDE and Formal Design Models by References to Domain Ontologies. A Model Annotation Based Approach....Pages 325-339
Towards Functional Requirements Analytics....Pages 340-357
Heterogeneous Semantics and Unifying Theories....Pages 358-373
Front Matter....Pages 374-394
Static and Runtime Verification, Competitors or Friends? (Track Summary)....Pages 395-395
StaRVOOrS — Episode II....Pages 397-401
A Model-Based Approach to Combining Static and Dynamic Verification Techniques....Pages 402-415
Information Flow Analysis for Go....Pages 416-430
Challenges in High-Assurance Runtime Verification....Pages 431-445
Static versus Dynamic Verification in Why3, Frama-C and SPARK 2014....Pages 446-460
Considering Typestate Verification for Quantified Event Automata....Pages 461-478
Combining Static and Runtime Methods to Achieve Safe Standing-Up for Humanoid Robots....Pages 479-495
On Combinations of Static and Dynamic Analysis – Panel Introduction....Pages 496-514
Safer Refactorings....Pages 515-516
Front Matter....Pages 517-531
Rigorous Engineering of Collective Adaptive Systems Track Introduction....Pages 533-533
Programming of CAS Systems by Relying on Attribute-Based Communication....Pages 535-538
Towards Static Analysis of Policy-Based Self-adaptive Computing Systems....Pages 539-553
A Calculus for Open Ensembles and Their Composition....Pages 554-569
Front Matter....Pages 570-588
Logic Fragments: Coordinating Entities with Logic Programs....Pages 533-533
Mixed-Critical Systems Design with Coarse-Grained Multi-core Interference....Pages 589-604
A Library and Scripting Language for Tool Independent Simulation Descriptions....Pages 605-621
Adaptation to the Unforeseen: Do we Master our Autonomous Systems? Questions to the Panel – Panel Introduction....Pages 622-638
Smart Coordination of Autonomic Component Ensembles in the Context of Ad-Hoc Communication....Pages 639-641
A Tool-Chain for Statistical Spatio-Temporal Model Checking of Bike Sharing Systems....Pages 642-656
Rigorous Graphical Modelling of Movement in Collective Adaptive Systems....Pages 657-673
Integration and Promotion of Autonomy with the ARE Framework....Pages 674-688
Safe Artificial Intelligence and Formal Methods....Pages 689-703
Engineering Adaptivity, Universal Autonomous Systems Ethics and Compliance Issues....Pages 704-713
Front Matter....Pages 714-719
Correctness-by-Construction and Post-hoc Verification: Friends or Foes?....Pages 721-721
Correctness-by-Construction and Post-hoc Verification: A Marriage of Convenience?....Pages 723-729
Deductive Verification of Legacy Code....Pages 730-748
Conditions for Compatibility of Components....Pages 749-765
A Logic for the Statistical Model Checking of Dynamic Software Architectures....Pages 766-783
On Two Friends for Getting Correct Programs....Pages 784-805
Proof-Carrying Apps: Contract-Based Deployment-Time Verification....Pages 806-820
Supervisory Controller Synthesis for Product Lines Using CIF 3....Pages 821-838
Partial Verification and Intermediate Results as a Solution to Combine Automatic and Interactive Verification Techniques....Pages 839-855
Front Matter....Pages 856-873
Security and Privacy of Protocols and Software with Formal Methods....Pages 874-880
A Model-Based Approach to Secure Multiparty Distributed Systems....Pages 881-881
Information Leakage Analysis of Complex C Code and Its application to OpenSSL....Pages 883-892
Integrated Modeling Workflow for Security Assurance....Pages 893-908
A Privacy-Aware Conceptual Model for Handling Personal Data....Pages 909-925
Guaranteeing Privacy-Observing Data Exchange....Pages 926-941
Back Matter....Pages 942-957
....Pages 958-969