Leveraging Applications of Formal Methods, Verification and Validation: Engineering Principles : 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20–30, 2020, Proceedings, Part II

The three-volume set LNCS 12476 - 12478 constitutes the refereed proceedings of the 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, which was planned to take place during October 20–30, 2020, on Rhodes, Greece. The event itself was postponed to 2021 due to the COVID-19 pandemic. The papers presented were carefully reviewed and selected for inclusion in the proceedings. Each volume focusses on an individual topic with topical section headings within the volume: **Part I, Verification Principles:** Modularity and (De-)Composition in Verification; X-by-Construction: Correctness meets Probability; 30 Years of Statistical Model Checking; Verification and Validation of Concurrent and Distributed Systems. **Part II, Engineering Principles:** Automating Software Re-Engineering; Rigorous Engineering of Collective Adaptive Systems. **Part III, Applications:** Reliable Smart Contracts: State-of-the-art, Applications, Challenges and Future Directions; Automated Verification of Embedded Control Software; Formal methods for DIStributed COmputing in future RAILway systems. Front Matter ....Pages i-xv Front Matter ....Pages 1-1 Automating Software Re-engineering (Serge Demeyer, Reiner Hähnle, Heiko Mantel)....Pages 3-8 Formal Verification of Developer Tests: A Research Agenda Inspired by Mutation Testing (Serge Demeyer, Ali Parsai, Sten Vercammen, Brent van Bladel, Mehrdad Abdi)....Pages 9-24 Modular Regression Verification for Reactive Systems (Alexander Weigl, Mattias Ulbrich, Daniel Lentzsch)....Pages 25-43 Finding Idioms in Source Code Using Subtree Counting Techniques (Dmitry Orlov)....Pages 44-54 Parametric Timed Bisimulation (Malte Lochau, Lars Luthmann, Hendrik Göttmann, Isabelle Bacher)....Pages 55-71 A Unifying Framework for Dynamic Monitoring and a Taxonomy of Optimizations (Marie-Christine Jakobs, Heiko Mantel)....Pages 72-92 Thirty-Seven Years of Relational Hoare Logic: Remarks on Its Principles and History (David A. Naumann)....Pages 93-116 Safer Parallelization (Reiner Hähnle, Asmae Heydari Tabar, Arya Mazaheri, Mohammad Norouzi, Dominic Steinhöfel, Felix Wolf)....Pages 117-137 Refactoring and Active Object Languages (Volker Stolz, Violet Ka I Pun, Rohit Gheyi)....Pages 138-158 Front Matter ....Pages 159-159 Rigorous Engineering of Collective Adaptive Systems Introduction to the 3rd Track Edition (Martin Wirsing, Rocco De Nicola, Stefan Jähnichen)....Pages 161-170 Composition of Component Models - A Key to Construct Big Systems (Wolfgang Reisig)....Pages 171-188 Degrees of Autonomy in Coordinating Collectives of Self-Driving Vehicles (Stefano Mariani, Franco Zambonelli)....Pages 189-204 Engineering Semantic Self-composition of Services Through Tuple-Based Coordination (Ashley Caselli, Giovanni Ciatto, Giovanna Di Marzo Serugendo, Andrea Omicini)....Pages 205-223 A Dynamic Logic for Systems with Predicate-Based Communication (Rolf Hennicker, Martin Wirsing)....Pages 224-242 Abstractions for Collective Adaptive Systems (Omar Inverso, Catia Trubiani, Emilio Tuosto)....Pages 243-260 Verifying AbC Specifications via Emulation (Rocco De Nicola, Tan Duong, Omar Inverso)....Pages 261-279 Adaptive Security Policies (Flemming Nielson, René Rydhof Hansen, Hanne Riis Nielson)....Pages 280-294 Capturing Dynamicity and Uncertainty in Security and Trust via Situational Patterns (Tomas Bures, Petr Hnetynka, Robert Heinrich, Stephan Seifermann, Maximilian Walter)....Pages 295-310 Guaranteeing Type Consistency in Collective Adaptive Systems (Jonas Schürmann, Tim Tegeler, Bernhard Steffen)....Pages 311-328 Epistemic Logic in Ensemble Specification (Jan Sürmeli)....Pages 329-343 FScaFi : A Core Calculus for Collective Adaptive Systems Programming (Roberto Casadei, Mirko Viroli, Giorgio Audrito, Ferruccio Damiani)....Pages 344-360 Writing Robotics Applications with X-Klaim (Lorenzo Bettini, Khalid Bourr, Rosario Pugliese, Francesco Tiezzi)....Pages 361-379 Measuring Adaptability and Reliability of Large Scale Systems (Valentina Castiglioni, Michele Loreti, Simone Tini)....Pages 380-396 Centrality-Preserving Exact Reductions of Multi-Layer Networks (Tatjana Petrov, Stefano Tognazzi)....Pages 397-415 Towards Dynamic Dependable Systems Through Evidence-Based Continuous Certification (Rasha Faqeh, Christof Fetzer, Holger Hermanns, Jörg Hoffmann, Michaela Klauck, Maximilian A. Köhl et al.)....Pages 416-439 Forming Ensembles at Runtime: A Machine Learning Approach (Tomáš Bureš, Ilias Gerostathopoulos, Petr Hnětynka, Jan Pacovský)....Pages 440-456 Synthesizing Control for a System with Black Box Environment, Based on Deep Learning (Simon Iosti, Doron Peled, Khen Aharon, Saddek Bensalem, Yoav Goldberg)....Pages 457-472 A Formal Model for Reasoning About the Ideal Fitness in Evolutionary Processes (Thomas Gabor, Claudia Linnhoff-Popien)....Pages 473-490 A Case Study of Policy Synthesis for Swarm Robotics (Paul Piho, Jane Hillston)....Pages 491-506 Maple-Swarm: Programming Collective Behavior for Ensembles by Extending HTN-Planning (Oliver Kosak, Lukas Huhn, Felix Bohn, Constantin Wanninger, Alwin Hoffmann, Wolfgang Reif)....Pages 507-524 Swarm and Collective Capabilities for Multipotent Robot Ensembles (Oliver Kosak, Felix Bohn, Lennart Eing, Dennis Rall, Constantin Wanninger, Alwin Hoffmann et al.)....Pages 525-540 Back Matter ....Pages 541-544 The three-volume set LNCS 12476 - 12478 constitutes the refereed proceedings of the 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, which was planned to take place during October 20-30, 2020, on Rhodes, Greece. The event itself was postponed to 2021 due to the COVID-19 pandemic. The papers presented were carefully reviewed and selected for inclusion in the proceedings. Each volume focusses on an individual topic with topical section headings within the volume: Part I, Verification Principles: Modularity and (De- )Composition in Verification; X-by-Construction: Correctness meets Probability; 30 Years of Statistical Model Checking; Verification and Validation of Concurrent and Distributed Systems. Part II, Engineering Principles: Automating Software Re-Engineering; Rigorous Engineering of Collective Adaptive Systems. Part III, Applications: Reliable Smart Contracts: State-of-the-art, Applications, Challenges and Future Directions; Automated Verification of Embedded Control Software; Formal methods for DIStributed COmputing in future RAILway systems