Program

October 21 (Saturday), 2017      (@Yannian Century Hotel, Changsha, China)

7:30-8:15: Registration

8:15-8:30: Opening co-located with FMAC 2017

8:30-9:30: Invited Talk of FMAC 2017

9:30-10:00: Coffee Break

10:00-11:40: Session - Analysis & Verification (Chair: Liqian Chen, 25min per talk)

- Taolue Chen, Yan Chen, Anthony W. Lin, Matthew Hague and Zhilin Wu,
     What's Decidable About String Constraints with ReplaceAll Function?

- Jiahong Jiang, Liqian Chen and Ji Wang,
     Generating Template Inductive Invariants via SMT Optimization

- Zhe Chen,
     Parametric Runtime Verification is NP-complete and coNP-complete

- Yong Li, Lei Song, Yuan Feng and Lijun Zhang,
     Verify LTL with Fairness Assumptions Efficiently

11:40-13:00: Lunch

13:00-14:40: Session - Probabilistic & Quantum Systems (Chair: Yuxin Deng, 25min per talk)

- Chao Huang, Xin Chen, Wang Lin, Zhengfeng Yang, Xuandong Li,
     Probabilistic Safety Verification of Stochastic Hybrid Systems Using Barrier Certificates

- Pengfei Yang, David N. Jansen and Lijun Zhang,
     Distribution-based Bisimulation for Labelled Markov Processes

- Andrea Turrini,
     Model Checking omega-regular Properties for Quantum Markov Chains

- Yangjia Li,
      Termination Analysis for Quantum Programs

14:40-15:00: Coffee Break

15:00-16:40: Session - Modeling & Controlling (Chair: Cong Tian, 25min per talk)

- Yi Li, Xiyue Zhang, Yuanyi Ji and Meng Sun,
      Capturing Stochastic and Real-Time Behavior in Reo Connectors

- Chao Huang, Xin Chen, Yifan Zhang, Shengchao Qin, Yifeng Zeng and Xuandong Li,
      Hierarchical Model Predictive Control for Switched Linear Multi-Robot Navigation

- Liming Li, Zhiping Shi, Yong Guan, Qianying Zhang and Yongdong Li,
      Formalization of geometric algebra in HOL Light

- Liyun Dai,
      Feye: A Tool for Identifyin g Semantic Differences Between Versions of Programs

16:40-17:00: Coffee Break

17:00-18:15: Session of FMAC 2017

18:20-20:00: Dinner