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