Formal Methods and Software Engineering: 19th International Conference on Formal Engineering Methods, ICFEM 2017, Xi’an, China, November 13-17, 2017, Proceedings

Front Matter ....Pages I-XVII
Front Matter ....Pages 1-1
 Towards Customizable CPS: Composability, Efficiency and Predictability  (Wang Yi)....Pages 3-15
Front Matter ....Pages 17-17
 Modularization of Refinement Steps for Agile Formal Methods  (Fabian Benduhn, Thomas Thüm, Ina Schaefer, Gunter Saake)....Pages 19-35
 Model Checking Pushdown Epistemic Game Structures  (Taolue Chen, Fu Song, Zhilin Wu)....Pages 36-53
 Transforming Timing Requirements into CCSL Constraints to Verify Cyber-Physical Systems  (Xiaohong Chen, Ling Yin, Yijun Yu, Zhi Jin)....Pages 54-70
 A Framework for Multi-view Reconciliation and for Medical Devices Personalization  (Yihai Chen, Bofang Zhang, Ridha Khedri, Huaikou Miao)....Pages 71-87
 Compiling Parameterized X86-TSO Concurrent Programs to Cubicle-\(\mathcal {W}\)  (Sylvain Conchon, David Declerck, Fatiha Zaïdi)....Pages 88-104
 Improving the Scalability of Automatic Linearizability Checking in SPIN  (Patrick Doolan, Graeme Smith, Chenyi Zhang, Padmanabhan Krishnan)....Pages 105-121
 Verifying Temporal Properties of C Programs via Lazy Abstraction  (Zhao Duan, Cong Tian, Zhenhua Duan)....Pages 122-139
 Combining Event-B and CSP: An Institution Theoretic Approach to Interoperability  (Marie Farrell, Rosemary Monahan, James F. Power)....Pages 140-156
 Refinement-Based Modelling and Verification of Design Patterns for Self-adaptive Systems  (Thomas Göthel, Nils Jähnig, Simon Seif)....Pages 157-173
 Assertion Generation Through Active Learning  (Long H. Pham, Ly Ly Tran Thi, Jun Sun)....Pages 174-191
 Detecting Energy Bugs in Android Apps Using Static Analysis  (Hao Jiang, Hongli Yang, Shengchao Qin, Zhendong Su, Jian Zhang, Jun Yan)....Pages 192-208
 A Flexible Approach for Finding Optimal Paths with Minimal Conflicts  (Juliana K. F. Bowles, Marco B. Caminati)....Pages 209-225
 A Certified Decision Procedure for Tree Shares  (Xuan-Bach Le, Thanh-Toan Nguyen, Wei-Ngan Chin, Aquinas Hobor)....Pages 226-242
 Classification-Based Parameter Synthesis for Parametric Timed Automata  (Jiaying Li, Jun Sun, Bo Gao, Étienne André)....Pages 243-261
 A Verification Framework for Stateful Security Protocols  (Li Li, Naipeng Dong, Jun Pang, Jun Sun, Guangdong Bai, Yang Liu et al.)....Pages 262-280
 A Sliding-Window Algorithm for On-The-Fly Interprocedural Program Analysis  (Xin Li, Mizuhito Ogawa)....Pages 281-297
 Exploring Design Alternatives for RAMP Transactions Through Statistical Model Checking  (Si Liu, Peter Csaba Ölveczky, Jatin Ganhotra, Indranil Gupta, José Meseguer)....Pages 298-314
 An Improved Android Collusion Attack Detection Method Based on Program Slicing  (Yunhao Liu, Xiaohong Li, Zhiyong Feng, Jianye Hao)....Pages 315-331
 Parameterized Complexity of Resilience Decision for Database Debugging  (Dongjing Miao, Zhipeng Cai)....Pages 332-344
 Formal Analysis of Linear Control Systems Using Theorem Proving  (Adnan Rashid, Osman Hasan)....Pages 345-361
 Policy Dependent and Independent Information Flow Analyses  (Manuel Töws, Heike Wehrheim)....Pages 362-378
 Improving Probability Estimation Through Active Probabilistic Model Learning  (Jingyi Wang, Xiaohong Chen, Jun Sun, Shengchao Qin)....Pages 379-395
 Nested Timed Automata with Diagonal Constraints  (Yuwei Wang, Yunqing Wen, Guoqiang Li, Shoji Yuen)....Pages 396-412
 Integration of Metamorphic Testing with Program Repair Methods Based on Adaptive Search Strategies and Program Equivalence  (Tingting Wu, Yunwei Dong, Tsong Yueh Chen, Mingyue Jiang, Man Lau, Fei-Ching Kuo et al.)....Pages 413-429
 Learning Types for Binaries  (Zhiwu Xu, Cheng Wen, Shengchao Qin)....Pages 430-446
 Inconsistency Analysis of Time-Based Security Policy and Firewall Policy  (Yi Yin, Yuichiro Tateiwa, Yun Wang, Yoshiaki Katayama, Naohisa Takahashi)....Pages 447-463
 An Algebraic Approach to Automatic Reasoning for NetKAT Based on Its Operational Semantics  (Yuxin Deng, Min Zhang, Guoqing Lei)....Pages 464-480
 Pareto Optimal Reachability Analysis for Simple Priced Timed Automata  (Zhengkui Zhang, Brian Nielsen, Kim Guldstrand Larsen, Gilles Nies, Marvin Stenger, Holger Hermanns)....Pages 481-495
Back Matter ....Pages 497-498