 |
08:50-09:00 | Opening |
|
09:00-10:00 |
Keynote I (online) Session Chair: Kazuhiro Ogata (JAIST) Program Verification: a 70+-Year History Moshe Y. Vardi (Rice University, USA) |
|
10:00-10:30 | Coffee Break & photos |
|
10:30-12:00 |
Session 1: Program Analysis I Session 1: Program Analysis I |
|
10:30-11:00 A wp Characterization of Jump Statements Wei Chen |
||
|
11:00-11:30 Behind Clint and Hoare's goto Proof Rule Wei Chen |
||
|
11:30-12:00 A Proof System for HRML with Extended Hoare Logic Ningning Chen, Huibiao Zhu and Huixing Fang |
||
|
12:00-14:00 | Lunch Break |
|
14:00-16:00 |
Session 2: Program Analysis II Session Chair: Xueyang Zhu (ISCAS) |
|
14:00-14:30
Dynamic Verification of C/C++11 Concurrency over Multi Copy Atomics Sanjana Singh, Divyanjali Sharma and Subodh Sharma
14:30-15:00
An Abstract Domain to Infer Linear Absolute Value Equalities
Liqian Chen, Banghu Yin, Dengping Wei and Ji Wang
15:00-15:30
Discovering Properties about Arrays via Path Dependence Analysis
Qianqian Zhang, Yao Zhang, Xiaohong Li and Bin Wu
15:30-16:00
Inferring Loop Invariants for Multi-Path Loops
Yingwen Lin, Yao Zhang, Sen Chen, Fu Song, Xiaofei Xie, Xiaohong Li and Lintan Sun |
||
|
16:00-16:30 | Coffee Break |
|
16:30-18:30 |
Session 3: System modeling and verification I Session Chair: Liqian Chen (NUDT) |
|
16:30-17:00
Parametric Spatio-temporal Modeling and Safety Verifying for T2T-CBTC Systems Qianzhu Zhao, Jing Liu and Xiang Chen
17:00-17:30
Verification of RoboSim Models Using UPPAAL
Mingzhuo Zhang, Dehui Du, Augusto Sampaio, Ana Cavalcanti, Madiel Conserva Filho and Menghan Zhang
17:30-18:00
A Formal Engineering Approach to Product Family Modeling
Xi Wang, Ridha Khedri and Weikai Miao
18:00-18:30
Encoding Induction Proof into Dafny
Hongjian Jiang, Yongjian Li, Sijun Tan and Yongxin Zhao |
||
Day 2 (August 26, 2020)Venue: (Multi-Function Hall, 3rd Floor, Yifu Building) |
||
|
09:00-10:00 |
Keynote II (online) Session Chair: Huibiao Zhu (ECNU) Advances of Proof Scores in CafeOBJ Kokichi Futatsugi (JAIST, JP) |
|
10:00-10:30 | Coffee Break |
|
10:30-12:00 |
Session 4: Real-Time Verification Session Chair: Xiaohong Chen (ECNU) |
|
10:30-11:00 VERDS: Modeling and Verification of Finite State Systems with Discrete Time Models by Symbolic Techniques Wenhui Zhang, Xue-Yang Zhu and Yulong Bao |
||
|
11:00-11:30 Reasoning About Real-Time Systems in Event-B Models with Fairness Assumptions Chenyang Zhu, Michael Butler, Corina Cirstea and Thai Son Hoang |
||
|
11:30-12:00 A Timed Automata based Automatic Framework for Verifying STL Properties of Simulink Models Miao Tian, Jianqi Shi, Zhe Hou, Yanhong Huang and Shengchao Qin |
||
|
12:00-14:00 | Lunch Break |
|
14:00-15:30 |
Session 5: Model Checking and Logics Session Chair: Wenhui Zhang (ISCAS) |
|
14:00-14:30
Petri Net Based CTL Model Checking: Using a New Method to Construct OBDD Variable Order Leifeng He and Guanjun Liu
14:30-15:00
Featured Games
Uli Fahrenberg and Axel Legay
15:00-15:30
On a specification theory for fuzzy modal logic
Manisha Jain, Leandro Gomes, Alexandre Madeira and Luís Soares Barbosa |
||
|
15:30-16:00 | Coffee Break |
|
16:00-17:30 |
Session 6: Requirement Engineering Session Chair: Guoqiang Li (SJTU)
16:00-16:30
Generating Test Cases from Requirements: A Case Study in Railway Control System Domain Hanyue Zheng, Jincao Feng, Weikai Miao and Geguang Pu
16:30-17:00
RE2B: enhancing correctness of both requirements and design models by integrating EBRE and Event-B Shiling Feng, Xiaohong Chen, Qin Li and Yongxin Zhao
17:00-17:30
Eliciting Timing Requirements for Cyber-Physical Systems: a Multiform Time based Approach Jiajia Yang, Xiaohong Chen and Ling Yin |
Day 3 (August 27, 2020)Venue: (Multi-Function Hall, 3rd Floor, Yifu Building) |
||
|
09:00-10:00 |
Keynote III Session Chair: Mingsong Chen (ECNU) The Research and Practice of Containers System Hai Jin (Huazhong University of Science and Technology, CN) |
|
10:00-10:30 | Coffee Break |
|
10:30-12:30 |
Session 7: System modeling and verification II Session Chair: Min Zhang (ECNU) |
|
10:30-11:00 A Parallel Implementation Of Liveness On Knowledge Graphs Under Label Constraints Qunhao Sha, Qizhe Yang and Guoqiang Li |
||
|
11:00-11:30 Exploring Design Alternatives for Replicated RAMP Transactions Using Maude Lei Liang and Si Liu |
||
|
11:30-12:00
A Character-Level Convolutional Neural Network for Predicting Exploitability of Vulnerability Jinghui Lv, Yude Bai, Zhenchang Xing, Xiaohong Li and Weimin Ge
12:00-12:30
Formal Modelling and Verification of the RTPS Behavior Module Jiaqi Yin, Huibiao Zhu, Yuan Fei and Qiwen Xu |
||
|
12:30-12:40 | Closing |