Program
Final Program for ICFEM 2017 Main Conference
Monday, 13 November 2017
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 |
Tuesday, 14 November 2017
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) |
Wednesday, 15 November 2017
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
Thursday, 16 November 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
Thursday, 16 November 2017
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
Thursday, 16 November 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
Thursday, 16 November 2017
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) |
Friday, 17 November 2017
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 |