| 2021 | Reasoning About Real-Time Systems in Event-B Models with Fairness Assumptions. | Chenyang Zhu, Michael J. Butler, Corina Crstea, Thai Son Hoang |
| 2021 | Generating Test Cases from Requirements: A Case Study in Railway Control System Domain. | Hanyue Zheng, Jincao Feng, Weikai Miao, Geguang Pu |
| 2021 | Parametric Spatio-temporal Modeling and Safety Verifying for T2T-CBTC Systems. | Qianzhu Zhao, Jing Liu, Xiang Chen, Tengfei Li, Junfeng Sun, Lipeng Zhang |
| 2021 | Discovering Properties about Arrays via Path Dependence Analysis. | Qianqian Zhang, Yao Zhang, Xiao-Hong Li, Bin Wu |
| 2021 | VERDS: Modeling and Verification of Finite State Systems with Discrete Time Models by Symbolic Techniques. | Wenhui Zhang, Xue-Yang Zhu, Yulong Bao |
| 2021 | Transforming RoboSim Models into UPPAAL. | Mingzhuo Zhang, Dehui Du, Augusto Sampaio, Ana Cavalcanti, Madiel Conserva Filho, Menghan Zhang |
| 2021 | Formal Modelling and Verification of the RTPS Behavior Module. | Jiaqi Yin, Huibiao Zhu, Yuan Fei, Qiwen Xu |
| 2021 | Eliciting Timing Requirements for Cyber-Physical Systems: a Multiform Time based Approach. | Jiajia Yang, Xiaohong Chen, Ling Yin |
| 2021 | A Formal Engineering Approach to Product Family Modeling. | Xi Wang, Ridha Khdri, Weikai Miao |
| 2021 | Program Verification: a 70+- Year History. | Moshe Y. Vardi |
| 2021 | A Timed Automata based Automatic Framework for Verifying STL Properties of Simulink Models. | Miao Tian, Jianqi Shi, Zhe Hou, Yanhong Huang, Shengchao Qin |
| 2021 | Dynamic Verification of C11 Concurrency over Multi Copy Atomics. | Sanjana Singh, Divyanjali Sharma, Subodh Sharma |
| 2021 | A Parallel Implementation of Liveness on Knowledge Graphs under Label Constraints. | Qunhao Sha, Qizhe Yang, Guoqiang Li |
| 2021 | A Character-Level Convolutional Neural Network for Predicting Exploitability of Vulnerability. | Jinghui Lyu, Yude Bai, Zhenchang Xing, Xiaohong Li, Weimin Ge |
| 2021 | Inferring Loop Invariants for Multi-Path Loops. | Yingwen Lin, Yao Zhang, Sen Chen, Fu Song, Xiaofei Xie, Xiaohong Li, Lintan Sun |
| 2021 | Exploring Design Alternatives for Replicated RAMP Transactions Using Maude. | Lei Liang, Si Liu |
| 2021 | Research and Practice of Container System. | Hai Jin |
| 2021 | Encoding Induction Proof in Dafny. | Hongjian Jiang, Yongjian Li, Sijun Tan, Yongxin Zhao |
| 2021 | Towards a specification theory for fuzzy modal logic. | Manisha Jain, Leandro Gomes, Alexandre Madeira, Lus Soares Barbosa |
| 2021 | Petri Net Based CTL Model Checking: Using a New Method to Construct OBDD Variable Order. | Leifeng He, Guanjun Liu |
| 2021 | Advances of Proof Scores in CafeOBJ : Invited Paper. | Kokichi Futatsugi |
| 2021 | RE2B: Enhancing Correctness of Both Requirements and Design Models. | Shiling Feng, Xiaohong Chen, Qin Li, Yongxin Zhao |
| 2021 | Featured Games. | Uli Fahrenberg, Axel Legay |
| 2021 | A Proof System for HRML with Extended Hoare Logic. | Ningning Chen, Huibiao Zhu, Huixing Fang |
| 2021 | An Abstract Domain to Infer Linear Absolute Value Equalities. | Liqian Chen, Banghu Yin, Dengping Wei, Ji Wang |