Formal Methods and Software Engineering : 21st International Conference on Formal Engineering Methods, ICFEM 2019, Shenzhen, China, November 5–9, 2019, Proceedings

This book constitutes the proceedings of the 21st International Conference on Formal Engineering Methods, ICFEM 2019, held in Shenzhen, China, in November 2019. The 28 full and 8 short papers presented in this volume were carefully reviewed and selected from 94 submissions. They deal with the recent progress in the use and development of formal engineering methods for software and system design and record the latest development in formal engineering methods. Front Matter ....Pages i-xxi Front Matter ....Pages 1-1 Secure Deep Learning Engineering: A Road Towards Quality Assurance of Intelligent Systems (Yang Liu, Lei Ma, Jianjun Zhao)....Pages 3-15 Front Matter ....Pages 17-17 Using DimSpec for Bounded and Unbounded Software Model Checking (Marko Kleine Büning, Tomáš Balyo, Carsten Sinz)....Pages 19-35 SMTBCF: Efficient Backbone Computing for SMT Formulas (Yueling Zhang, Geguang Pu, Min Zhang)....Pages 36-51 Automatic Verification for Node-Based Visual Script Notation Using Model Checking (Isamu Hasegawa, Tomoyuki Yokogawa)....Pages 52-68 A Reo Model of Software Defined Networks (Hui Feng, Farhad Arbab, Marcello Bonsangue)....Pages 69-85 Design of Point-and-Click User Interfaces for Proof Assistants (Bohua Zhan, Zhenyan Ji, Wenfan Zhou, Chaozhu Xiang, Jie Hou, Wenhui Sun)....Pages 86-103 SqlSol: An accurate SQL Query Synthesizer (Lin Cheng)....Pages 104-120 Towards Verifying Ethereum Smart Contracts at Intermediate Language Level (Ximeng Li, Zhiping Shi, Qianying Zhang, Guohui Wang, Yong Guan, Ning Han)....Pages 121-137 Simulations for Multi-Agent Systems with Imperfect Information (Patrick Gardy, Yuxin Deng)....Pages 138-153 On the Generation of Equational Dynamic Logics for Weighted Imperative Programs (Leandro Gomes, Alexandre Madeira, Manisha Jain, Luis S. Barbosa)....Pages 154-169 A Security Calculus for Wireless Networks of Named Data Networking (Yuan Fei, Huibiao Zhu, Haiying Sun, Jiaqi Yin)....Pages 170-185 Automatic Modularization of Large Programs for Bounded Model Checking (Marko Kleine Büning, Carsten Sinz)....Pages 186-202 PDNet: A Programming Language for Software-Defined Networks with VLAN (Shuangqing Xiang, Marcello Bonsangue, Huibiao Zhu)....Pages 203-218 Consistency Enforcement for Static First-Order Invariants in Sequential Abstract State Machines (Klaus-Dieter Schewe)....Pages 219-235 Probably Approximate Safety Verification of Hybrid Dynamical Systems (Bai Xue, Martin Fränzle, Hengjun Zhao, Naijun Zhan, Arvind Easwaran)....Pages 236-252 A Formally Verified Algebraic Approach for Dynamic Reliability Block Diagrams (Yassmeen Elderhalli, Osman Hasan, Sofiène Tahar)....Pages 253-269 Reasoning About Universal Cubes in MCMT (Sylvain Conchon, Mattias Roux)....Pages 270-285 sCompile: Critical Path Identification and Analysis for Smart Contracts (Jialiang Chang, Bo Gao, Hao Xiao, Jun Sun, Yan Cai, Zijiang Yang)....Pages 286-304 A Mechanized Theory of Program Refinement (Boubacar Demba Sall, Frédéric Peschanski, Emmanuel Chailloux)....Pages 305-321 A Relational Static Semantics for Call Graph Construction (Xilong Zhuo, Chenyi Zhang)....Pages 322-335 Solution Enumeration Abstraction: A Modeling Idiom to Enhance a Lightweight Formal Method (Allison Sullivan, Darko Marinov, Sarfraz Khurshid)....Pages 336-352 Formal Analysis of Qualitative Long-Term Behaviour in Parametrised Boolean Networks (Nikola Beneš, Luboš Brim, Samuel Pastva, Jakub Poláček, David Šafránek)....Pages 353-369 Combining Parallel Emptiness Checks with Partial Order Reductions (Denis Poitrenaud, Etienne Renault)....Pages 370-386 A Coalgebraic Semantics Framework for Quantum Systems (Ai Liu, Meng Sun)....Pages 387-402 Parameterized Hardware Verification Through a Term-Level Generalized Symbolic Trajectory Evaluation (Yongjian Li, Bow-yaw Wang)....Pages 403-419 An Axiomatisation of the Probabilistic \(\mu \)-Calculus (Junnan Xu, Wanwei Liu, David N. Jansen, Lijun Zhang)....Pages 420-437 Synthesizing Nested Ranking Functions for Loop Programs via SVM (Yi Li, Xuechao Sun, Yong Li, Andrea Turrini, Lijun Zhang)....Pages 438-454 A First Step in the Translation of Alloy to Coq (Salwa Souaf, Frédéric Loulergue)....Pages 455-469 Assessment of a Formal Requirements Modeling Approach on a Transportation System (Steve Jeffrey Tueno Fotso, Régine Laleau, Marc Frappier, Amel Mammar, Francois Thibodeau, Mama Nsangou Mouchili)....Pages 470-486 Front Matter ....Pages 487-487 Design Model Repair with Formal Verification (Cheng-Hao Cai, Jing Sun, Gillian Dobbie)....Pages 489-492 A Performance-Sensitive Malware Detection System on Mobile Platform (Ruitao Feng, Yang Liu, Shangwei Lin)....Pages 493-497 Certifying Hardware Model Checking Results (Zhengqi Yu, Armin Biere, Keijo Heljanko)....Pages 498-502 A Note on Failure Mode Reasoning (Hamid Jahanian)....Pages 503-506 Robustness of Piece-Wise Linear Neural Network with Feasible Region Approaches (Jay Hoon Jung, YoungMin Kwon)....Pages 507-511 Formal Specification and Verification of Smart Contracts (Jiao Jiao)....Pages 512-516 Spatio-Temporal Specification Language for Cyber-Physical Systems (Tengfei Li)....Pages 517-521 A Modeling Framework of Cyber-Physical-Social Systems with Human Behavior Classification Based on Machine Learning (Dongdong An, Jing Liu, Xiaohong Chen, Tengfei Li, Ling Yin)....Pages 522-525 Back Matter ....Pages 527-528