Formal methods and software engineering : 20th international conference on formal engineering methods, ICFEM 2018, Gold Coast, QLD, Australia, November 12-16, 2018 : proceedings

This book constitutes the refereed proceedings of the 20th International Conference on Formal Engineering Methods, ICFEM 2018, held in Gold Coast, QLD, Australia, in November 2018. The 22 revised full papers presented together with 14 short papers were carefully reviewed and selected from 66 submissions. The conference focuses on all areas related to formal engineering methods, such as verification; network systems; type theory; theorem proving; logic and semantics; refinement and transition systems; and emerging applications of formal methods. Front Matter ....Pages I-XXII Front Matter ....Pages 1-1 Engineering a Theory of Concurrent Programming (Ian J. Hayes)....Pages 3-18 Front Matter ....Pages 19-19 Behaviour-Driven Formal Model Development (Colin Snook, Thai Son Hoang, Dana Dghyam, Michael Butler, Tomas Fischer, Rupert Schlick et al.)....Pages 21-36 The Foul Adversary: Formal Models (Naipeng Dong, Tim Muller)....Pages 37-53 The Miles Before Formal Methods - A Case Study on Modeling and Analyzing a Passenger Lift System (Teck Ping Khoo, Jun Sun)....Pages 54-69 PAR: A Practicable Formal Method and Its Supporting Platform (Jinyun Xue, Yujun Zheng, Qimin Hu, Zhen You, Wuping Xie, Zhuo Cheng)....Pages 70-86 Front Matter ....Pages 87-87 Deductive Verification of Hybrid Control Systems Modeled in Simulink with KeYmaera X (Timm Liebrenz, Paula Herber, Sabine Glesner)....Pages 89-105 Verification of Strong Nash-equilibrium for Probabilistic BAR Systems (Dileepa Fernando, Naipeng Dong, Cyrille Jegourel, Jin Song Dong)....Pages 106-123 Model Checking of C++ Programs Under the x86-TSO Memory Model (Vladimír Štill, Jiří Barnat)....Pages 124-140 Front Matter ....Pages 141-141 Modeling and Verifying NDN Access Control Using CSP (Yuan Fei, Huibiao Zhu)....Pages 143-159 The Power of Synchronisation: Formal Analysis of Power Consumption in Networks of Pulse-Coupled Oscillators (Paul Gainer, Sven Linker, Clare Dixon, Ullrich Hustadt, Michael Fisher)....Pages 160-176 CDGDroid: Android Malware Detection Based on Deep Learning Using CFG and DFG (Zhiwu Xu, Kerong Ren, Shengchao Qin, Florin Craciun)....Pages 177-193 Front Matter ....Pages 195-195 Strongly Typed Numerical Computations (Matthieu Martel)....Pages 197-214 Type Capabilities for Object-Oriented Programming Languages (Xi Wu, Yi Lu, Patrick A. Meiring, Ian J. Hayes, Larissa A. Meinicke)....Pages 215-230 Capabilities: Effects for Free (Aaron Craig, Alex Potanin, Lindsay Groves, Jonathan Aldrich)....Pages 231-247 Front Matter ....Pages 249-249 A Framework for Interactive Verification of Architectural Design Patterns in Isabelle/HOL (Diego Marmsoler)....Pages 251-269 Formalization of Symplectic Geometry in HOL-Light (Guohui Wang, Yong Guan, Zhiping Shi, Qianying Zhang, Xiaojuan Li, Yongdong Li)....Pages 270-283 Using Theorem Provers to Increase the Precision of Dependence Analysis for Information Flow Control (Bernhard Beckert, Simon Bischof, Mihai Herda, Michael Kirsten, Marko Kleine Büning)....Pages 284-300 Front Matter ....Pages 301-301 Preserving Liveness Guarantees from Synchronous Communication to Asynchronous Unstructured Low-Level Languages (Nils Berg, Thomas Göthel, Armin Danziger, Sabine Glesner)....Pages 303-319 Deriving Mode Logic for Autonomous Resilient Systems (Inna Vistbakka, Amin Majd, Elena Troubitsyna)....Pages 320-336 UTP Semantics for BigrTiMo (Wanling Xie, Huibiao Zhu, Shengchao Qin)....Pages 337-353 Front Matter ....Pages 355-355 Analysis on Strategies of Superposition Refinement of Event-B Specifications (Tsutomu Kobayashi, Fuyuki Ishikawa)....Pages 357-372 Formalising Extended Finite State Machine Transition Merging (Michael Foster, Ramsay G. Taylor, Achim D. Brucker, John Derrick)....Pages 373-387 Checking Activity Transition Systems with Back Transitions Against Assertions (Cunjing Ge, Jiwei Yan, Jun Yan, Jian Zhang)....Pages 388-403 Front Matter ....Pages 405-405 Towards Trustworthy AI for Autonomous Systems (Hadrien Bride, Jin Song Dong, Zhé Hóu, Brendan Mahony, Martin Oxenham)....Pages 407-411 Towards Dependable and Explainable Machine Learning Using Automated Reasoning (Hadrien Bride, Jie Dong, Jin Song Dong, Zhé Hóu)....Pages 412-416 Front Matter ....Pages 417-417 Modeling and Verification of Component Connectors (Xiyue Zhang)....Pages 419-422 Model Based Testing of Cyber-Physical Systems (Teck Ping Khoo)....Pages 423-426 Service-Oriented Design and Verification of Hybrid Control Systems (Timm Liebrenz)....Pages 427-431 Developing Reliable Component-Based Software in Mediator (Yi Li)....Pages 432-435 Model Checking Nash-Equilibrium - Automatic Verification of Robustness in Distributed Systems (Dileepa Fernando)....Pages 436-440 Analyzing Security and Privacy in Design and Implementation of Web Authentication Protocols (Kailong Wang)....Pages 441-445 Combining Deep Learning and Probabilistic Model Checking in Sports Analytics (Kan Jiang)....Pages 446-449 Security Analysis of Smart Home Implementations (Kulani Mahadewa)....Pages 450-454 Principled Greybox Fuzzing (Yuekang Li)....Pages 455-458 Engineering Software for Modular Formalisation and Verification of STV Algorithms (Milad K. Ghale)....Pages 459-463 Towards Building a Generic Vulnerability Detection Platform by Combining Scalable Attacking Surface Analysis and Directed Fuzzing (Xiaoning Du)....Pages 464-468 Formalising Performance Guarantees in Meta-Reinforcement Learning (Amanda Mahony)....Pages 469-472 Back Matter ....Pages 473-474 This book constitutes the refereed proceedings of the 15th International Conference on Formal Engineering Methods, ICFEM 2013, held in Queenstown, New Zealand, in October/November 2013. The 28 revised full papers together with 2 keynote speeches presented were carefully reviewed and selected from 88 submissions. The topics covered are abstraction and refinement, formal specification and modeling, program analysis, software verification, formal methods for software safety, security, reliability and dependability, tool development, integration and experiments involving verified systems, formal methods used in certifying products under international standards, and formal model-based development and code generation.