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