ICFEM 2017

Final Program for ICFEM 2017 Main Conference

8:00 ~ 8:45	Registration
8:45 ~ 9:00	Opening
9:00 ~ 10:00	Keynote Speech (Chair: Shaoying Liu)   The Challenges of Probabilistic Thinking   David S. Rosenblum
10:00 ~ 10:30	Coffee Break
10:30 ~ 12:00	Program Analysis (Chair: Shengchao Qin)   Policy Dependent and Independent Information Flow Analyses   Manuel Töws and Heike Wehrheim   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 and Sebastian Ng   An Improved Android Collusion Attack Detection Method Based on Program Slicing   Yunhao Liu, Xiaohong Li, Zhiyong Feng and Jianye Hao
12:00 ~ 14:00	Lunch
14:00 ~ 15:30	Program Analysis (Chair: Jun Sun)   Detecting Energy Bugs in Android Apps Using Static Analysis   Hao Jiang, Hongli Yang, Shengchao Qin, Zhendong Su, Jian Zhang and Jun Yan   A Sliding-Window Algorithm for On-The-Fly Interprocedural Program Analysis   Xin Li and Mizuhito Ogawa   Learning Types for Binaries   Zhiwu Xu, Cheng Wen and Shengchao Qin
15:30 ~ 16:00	Coffee Break
16:00 ~ 18:00	Modeling (Chair: Guoqiang Li)   Improving Probability Estimation through Active Probabilistic Model Learning   Jingyi Wang, Xiaohong Chen, Jun Sun and Shengchao Qin   A Certified Decision Procedure for Tree Shares   Xuan Bach Le, Thanh Toan Nguyen, Wei-Ngan Chin and Aquinas Hobor   A Framework of Multi-view Reconciliation for Medical Device Software   Yihai Chen, Bofang Zhang, Ridha Khedri and Huaikou Miao   A Flexible Approach for Finding Optimal Paths with Minimal Conflicts   Juliana Küster Filipe Bowles and Marco B. Caminati

8:00 ~ 9:00	Registration
9:00 ~ 10:00	Keynote Speech (Chair: Luke Ong)   A Logical Revolution   Moshe Y. Vardi
10:00 ~ 10:30	Coffee Break
10:30 ~ 12:00	Formal Analysis (Chair: Zijiang Yang)   Parameterized Complexity of Resilience Decision for Database Debugging   Dongjing Miao and Zhipeng Cai   Improving the Scalability of Automatic Linearizability Checking in SPIN   Patrick Doolan, Graeme Smith, Chenyi Zhang and Padmanabhan Krishnan   Modularization of Refinement Steps for Agile Formal Methods   Fabian Benduhn, Thomas Thüm, Ina Schaefer and Gunter Saake
12:00 ~ 14:00	Lunch
14:00 ~ 15:30	Timed Automata (Chair: Huaikou Miao)   Classification Based Parameter Synthesis for Parametric Timed Automata   Jiaying Li, Jun Sun, Bo Gao and Étienne André   Pareto Optimal Reachability Analysis for Simple Priced Timed Automata   Zhengkui Zhang, Brian Nielsen, Kim Guldstrand Larsen, Gilles Nies, Marvin Stenger and Holger Hermanns   Nested Timed Automata with Diagonal Constraints   Guoqiang Li, Yuwei Wang, Yunqing Wen and Shoji Yuen
15:30 ~ 16:00	Coffee Break
16:00 ~ 17:30	Verification (Chair: Jinsong Dong)   Transforming Timing Requirements into CCSL Constraints to Verify Cyber-Physical Systems   Xiaohong Chen, Ling Yin, Yijun Yu and Zhi Jin   Refinement-Based Modelling and Verification of Design Patterns for Self-Adaptive Systems   Thomas Göthel, Nils Jähnig and Simon Seif   Formal Analysis of Linear Control Systems Using Theorem Proving   Adnan Rashid and Osman Hasan
18:30	Banquet (Chang le gong)

8:00 ~ 9:00	Registration
9:00 ~ 10:00	Keynote Speech (Chair: Zhenhua Duan)   Towards Customizable CPS: Composability, Efficiency and Predictability   Yi Wang
10:00 ~ 10:30	Coffee Break
10:30 ~ 12:00	Specification and Languages (Chair: Fumiko Nagoya)   An Algebraic Approach to Automatic Reasoning for NetKATBased on its Operational Semantics   Min Zhang, Yuxin Deng and Guoqing Lei   Combining Event-B and CSP: An Institution Theoretic Approach to Interoperability   Marie Farrell, Rosemary Monahan and James Power   Assertion Generation through Active Learning   Long H. Pham, Ly Ly Tran Thi and Jun Sun
12:00 ~ 14:00	Lunch
14:00 ~ 15:30	Model Checking (Chair: Wenhui Zhang)   Model Checking Pushdown Epistemic Game Structures   Taolue Chen, Fu Song and Zhilin Wu   Exploring Design Alternatives for RAMP Transactions through Statistical Model Checking   Si Liu, Peter Csaba Ölveczky, Jatin Ganhotra, Indranil Gupta and José Meseguer   Model Checking Safety Properties of Parameterized x86-TSO Programs   Sylvain Conchon, David Declerck and Fatiha Zaidi
15:30 ~ 16:00	Coffee Break
16:00 ~ 17:30	Security (Chair: Dines Bjorner)   A Verification Framework for Stateful Security Protocols   Li Li, Naipeng Dong, Jun Pang, Jun Sun, Guangdong Bai, Yang Liu and Jinsong Dong   Verifying Temporal Properties of C Programs via Lazy Abstraction   Zhao Duan and Cong Tian   Inconsistency Analysis of Time-Based Security Policy and Firewall Policy   Yi Yin, Yun Wang, Yuichiro Tateiwa, Yoshiaki Katayama and Naohisa Takahashi
17:30 ~ 17:45	Closing

SOFL+MSVL 2017

8:00 ~ 9:00	Registration
9:00 ~ 10:00	Invited talk (Chair: Zhenhua Duan)   New Inductive Invariants for Concurrency   Luke Ong
10:00 ~ 10:30	Coffee Break
10:30 ~ 11:50	Session 1(Chair: Jinyun Xue)   Implementing MapReduce with MSVL   Nan Zhang, Zhenhua Duan, Cong Tian, Meng Wang and Jin Cui   Graphically perceiving characteristics of the MCS lock and model checking them   Tam Nguyen and Kazuhiro Ogata   Foundation of A Framework to Support Compliance Checking in Construction Industry   Wuwei Shen, Guangyuan Li, Chung-Ling Lin and Hongliang Liang   The Complexity of Linear-time Temporal Logic Model Repair   Xiuting Tao and Guoqiang Li
11:50 ~ 14:00	Lunch
14:00 ~ 15:40	Session 2(Chair: Huaikou Miao)   A Software Tool to Support Scenario-Based Formal Specification for Error Prevention   Siyuan Li and Shaoying Liu   An Investigation of integrating a GUI-Aided Approach and a Specification-based Testing   Fumiko Nagoya and Shaoying Liu   A Software Tool to Support the "Vibration" Method   Pan Zhao and Shaoying Liu   A Framework Based on MSVL for Verifying Probabilistic Properties in Social Networks   Xiaobing Wang, Liyuan Ren and Liang Zhao   An Improved Reliability Test Model Construction Method Based on SOFL   Zhouxian Jiang, Honghui Li and Xuetao Tian
15:40 ~ 16:10	Coffee Break
16:10 ~ 17:30	Session 3(Chair: Guangyuan Li)   A proof score approach to formal verification of an imperative programming language compiler   Dorian Daudier, Trinh Ngoc Quoc Bao and Kazuhiro Ogata   Boosting UPPAAL for OSEK/VDX Applications with a Sequentialization Approach   Haitao Zhang, Zhuo Cheng, Jianxin Xue and Yonggang Lu   On the Cooperative Searching Problem   Chin-Fu Lin, Ondrej Navratil and Sheng-Lung Peng   Extending UML for Model Checking   Xinfeng Shu and Mengnan Wang
17:30 ~ 17:45	Closing

IMPEX2017

9:00 ~ 9:15	Introduction of the topics for IMPEX2017
9:15 ~ 10:15	Keynote Speech (Chair: Dominique Méry)   The Manifest Domain Analysis & Description Approach to Implicit and Explicit Semantics   Professor Dines Bjorner
10:15 ~ 10:30	Coffee Break
10:30 ~ 12:15	Position Papers (Chair: Régine Laleau)   Formal modeling of ontologies within Event-B   Idir Ait-Sadoune and Yamine Ait Ameur   Parameterized Model Checking Modulo Weak Memory Models   Sylvain Conchon   Explicit modelling of physical measures From Event-B to Java   Paul Gibson   Title to be announced   Elena Troubitsina
12:15 ~ 12:20	Conclusion and Perspectives

FM&MDD 2017

13:30 ~ 14:30	Invited talk   Dominique Mery
14:30 ~ 15:30	Technical talks   A Formal Model to Facilitate Security Testing in Modern Automotive Systems   Eduardo Dos Santos, Dominik Schoop and Andrew Simpson   Securing Open Source Clouds Using Models   Irum Rauf and Elena Troubitsyna
15:30 ~ 16:00	Coffee Break
16:00 ~ 17:00	Technical talks   Incremental Database Design using UML-B and Event-B   Ahmed Al-Brashdi, Michael Butler and Abdolbaghi Rezazadeh   Towards Integrated Modelling of Dynamic Access Control with UML and Event-B   Inna Vistbakka and Elena Troubitsyna
17:00 ~ 18:00	Invited talk   Regine Laleau
18:00 ~ 18:10	Closing

The 10th NSFC-JSPS Joint Workshop on Formal Methods

10:30 ~ 12:00	Session 1 (Chair: Shoji Yuen)   TBA   Mizuhito Ogawa (JAIST)   Decidability of Epsilon Popping PDA   Yuxi Fu (SJTU)
12:00 ~ 14:00	Lunch
14:30 ~ 16:00	Session 2 (Chair: Yijia Chen)   Zone Based Reachability Analysis of Timed Pushdown Automata with Freezing Clocks   Shoji Yuen (Nagoya)   Reachability Analysis of Conditional Pushdown Systems with Patterns   Xin Li (ECNU)
16:00 ~ 16:15	Coffee Break
16:15 ~ 17:45	Session 3 (Chair: Ming Zhang)   When does the Quantifier Rank Hierarchy of First-order Logic Collapse?   Yijia Chen (Fudan)   MRDP Theorem and Arithmetic   Keita Yokoyama (JAIST)

9:00 ~ 10:30	Session 1 (Chair: Yuxi Fu)   Decomposition Instead of Self-Composition for Proving the Absence of Timing Channels   Tachio Terauchi (Waseda)   Non-polynomial Worst-Case Analysis of Recursive Programs   Hongfei Fu (SJTU)
10:30 ~ 10:45	Coffee Break
10:45 ~ 12:15	Session 2 (Chair: Yijia Chen)   Z for Call-by-value   Koji Nakazawa (Nagoya)   On the Decidability of Functionality of Linear Multi Bottom-up Tree Transducers   Kenji Hashimoto (Nagoya)
12:15 ~ 12:30	Closing