Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice: 8th International Symposium, ISoLA 2018, Limassol, Cyprus, November 5-9, 2018, Proceedings, Part IV

Front Matter ....Pages I-XIV
Front Matter ....Pages 1-1
 RV-TheToP: Runtime Verification from Theory to the Industry Practice (Track Introduction)  (Ezio Bartocci, Yliès Falcone)....Pages 3-8
 Opportunities and Challenges in Monitoring Cyber-Physical Systems Security  (Borzoo Bonakdarpour, Jyotirmoy V. Deshmukh, Miroslav Pajic)....Pages 9-18
 Migrating Monitors + ABE: A Suitable Combination for Secure IoT?  (Gordon J. Pace, Pablo Picazo-Sanchez, Gerardo Schneider)....Pages 19-24
 Capturing Inter-process Communication for Runtime Verification on Android  (Alex Villazón, Haiyang Sun, Walter Binder)....Pages 25-31
 Considering Academia-Industry Projects Meta-characteristics in Runtime Verification Design  (Christian Colombo, Gordon J. Pace)....Pages 32-41
 Flexible Monitor Deployment for Runtime Verification of Large Scale Software  (Teng Zhang, Gregory Eakman, Insup Lee, Oleg Sokolsky)....Pages 42-50
 Increasing the Reusability of Enforcers with Lifecycle Events  (Oliviero Riganelli, Daniela Micucci, Leonardo Mariani)....Pages 51-57
 BDDs on the Run  (Klaus Havelund, Doron Peled)....Pages 58-69
 Verifying Real-World Software with Contracts for Concurrency  (João M. Lourenço)....Pages 70-73
Front Matter ....Pages 75-75
 Formal Methods in Industrial Practice - Bridging the Gap (Track Summary)  (Michael Felderer, Dilian Gurov, Marieke Huisman, Björn Lisper, Rupert Schlick)....Pages 77-81
 Model-Based Testing for Avionic Systems Proven Benefits and Further Challenges  (Jan Peleska, Jörg Brauer, Wen-ling Huang)....Pages 82-103
 Test Case Generation with PathCrawler/LTest: How to Automate an Industrial Testing Process  (Sébastien Bardin, Nikolai Kosmatov, Bruno Marre, David Mentré, Nicky Williams)....Pages 104-120
 Pitfalls in Applying Model Learning to Industrial Legacy Software  (Omar al Duhaiby, Arjan Mooij, Hans van Wezep, Jan Friso Groote)....Pages 121-138
 Formal Verification in Automotive Industry: Enablers and Obstacles  (Mattias Nyberg, Dilian Gurov, Christian Lidström, Andreas Rasmusson, Jonas Westman)....Pages 139-158
 Scalability of Deductive Verification Depends on Method Call Treatment  (Alexander Knüppel, Thomas Thüm, Carsten Padylla, Ina Schaefer)....Pages 159-175
 Java Automated Deductive Verification in Practice: Lessons from Industrial Proof-Based Projects  (David R. Cok)....Pages 176-193
 Security Filters for IoT Domain Isolation  (Dominique Bolignano, Florence Plateau)....Pages 194-211
 20 Years of UPPAAL Enabled Industrial Model-Based Validation and Beyond  (Kim G. Larsen, Florian Lorber, Brian Nielsen)....Pages 212-229
 Verification of Operating System Monolithic Kernels Without Extensions  (Evgeny Novikov, Ilja Zakharov)....Pages 230-248
 A Proposal of an Example and Experiments Repository to Foster Industrial Adoption of Formal Methods  (Rupert Schlick, Michael Felderer, Istvan Majzik, Roberto Nardone, Alexander Raschke, Colin Snook et al.)....Pages 249-272
Front Matter ....Pages 273-273
 Reliable Smart Contracts: State-of-the-Art, Applications, Challenges and Future Directions  (César Sánchez, Gerardo Schneider, Martin Leucker)....Pages 275-279
 Smart Contracts and Opportunities for Formal Methods  (Andrew Miller, Zhicheng Cai, Somesh Jha)....Pages 280-299
 Contracts over Smart Contracts: Recovering from Violations Dynamically  (Christian Colombo, Joshua Ellul, Gordon J. Pace)....Pages 300-315
 Security Analysis of Smart Contracts in Datalog  (Petar Tsankov)....Pages 316-322
 Temporal Properties of Smart Contracts  (Ilya Sergey, Amrit Kumar, Aquinas Hobor)....Pages 323-338
 Temporal Aspects of Smart Contracts for Financial Derivatives  (Christopher D. Clack, Gabriel Vanca)....Pages 339-355
 Marlowe: Financial Contracts on Blockchain  (Pablo Lamela Seijas, Simon Thompson)....Pages 356-375
 SMT-Based Verification of Solidity Smart Contracts  (Leonardo Alt, Christian Reitwiessner)....Pages 376-388
 Blockchains as Kripke Models: An Analysis of Atomic Cross-Chain Swap  (Yoichi Hirai)....Pages 389-404
 A Language-Independent Approach to Smart Contract Verification  (Xiaohong Chen, Daejun Park, Grigore Roşu)....Pages 405-413
 Towards Adding Variety to Simplicity  (Nachiappan Valliappan, Solène Mirliaz, Elisabet Lobo Vesga, Alejandro Russo)....Pages 414-431
 Fun with Bitcoin Smart Contracts  (Massimo Bartoletti, Tiziana Cimoli, Roberto Zunino)....Pages 432-449
 Computing Exact Worst-Case Gas Consumption for Smart Contracts  (Matteo Marescotti, Martin Blicha, Antti E. J. Hyvärinen, Sepideh Asadi, Natasha Sharygina)....Pages 450-465
Front Matter ....Pages 467-467
 Digital Transformation Trends: Industry 4.0, Automation, and AI  (Axel Hessenkämper, Falk Howar, Andreas Rausch)....Pages 469-471
 A Methodology for Combinatory Process Synthesis: Process Variability in Clinical Pathways  (Tristan Schäfer, Frederik Möller, Anja Burmann, Yevgen Pikus, Norbert Weißenberg, Marcus Hintze et al.)....Pages 472-486
 Automatic Composition of Rough Solution Possibilities in the Target Planning of Factory Planning Projects by Means of Combinatory Logic  (Jan Winkels, Julian Graefenstein, Tristan Schäfer, David Scholz, Jakob Rehof, Michael Henke)....Pages 487-503
 GOLD: Global Organization aLignment and Decision - Towards the Hierarchical Integration of Heterogeneous Business Models  (Barbara Steffen, Steve Boßelmann)....Pages 504-527
Back Matter ....Pages 529-530