We are grateful to conduct research sponsored by NSFC, CCF and multiple industrial partners including Huawei, Alibaba Group, and Ant Group. Recently, we are mainly working on the following exciting research themes.
We mean safe like nuclear safety as opposed to safe as in ‘trust and safety’ - Ilya Sutskever
Modern systems, including emerging AI models (e.g., deep neural networks) and AI-based systems (e.g., autonomous cars, autonomous systems, etc), are mostly built upon software, making it vital to ensure their trustworthiness from a software engineering perspective. In this line of research, we are working towards a systematic testing, verification and repair framework to evaluate, identify and fix the risks hidden in the AI models or AI-empowered systems, from different dimensions such as robustness, fairness, copyright and safety. This is crucial for stakeholders and AI-empowered industries to be aware of, manage and mitigate the safety and ethic risks in the new AI era.
Related selected publications: [ICSE 25, RA-L 24, TOSEM 24, ICSE 24, ISSTA 24, TDSC 24, ICSE Demo 23, ISSTA 23, S&P 22, ICSE 22, TOSEM 22, ASE 22, ICSE 21, TSE 21, TACAS 21, ISSTA 21, IJCIP, ICSE 20, ASE 20, ICECCS 20, ICSE 19]
Sample Work:
[ICSE 2024] Jianan Ma, Pengfei Yang, Jingyi Wang*, Youcheng Sun, Chengchao Huang and Zhen Wang. VeRe: Verification Guided Synthesis for Repairing Deep Neural Networks. 46th International Conference on Software Engineering, Lisbon, Portugal, Apr, 2024.
[S&P 2022] Jialuo Chen, Jingyi Wang*, Tinglan Peng, Youcheng Sun, Peng Cheng, Shouling Ji, Xingjun Ma, Bo Li and Dawn Song. Copy, Right? A Testing Framework for Copyright Protection of Deep Learning Models. 43rd IEEE Symposium on Security and Privacy, Oakland, USA, May 2022.
[TACAS 2021] Pengfei Yang, Renjue Li, Jianlin Li, Cheng-Chao Huang, Jingyi Wang, Jun Sun, Bai Xue and Lijun Zhang. Improving Neural Network Verification through Spurious Region Guided Refinement, 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Luxembourg, Luxembourg (online), Apr 2021.
[ICSE 2021] Jingyi Wang, Jialuo Chen, Youcheng Sun, Xingjun Ma, Dongxia Wang, Jun Sun and Peng Cheng. RobOT: Robustness-Oriented Testing for Deep Learning Systems. 43rd International Conference on Software Engineering, Madrid, Spain, May 2021.
[ICSE 2020] Peixin Zhang, Jingyi Wang*, Jun Sun, Guoliang Dong, Xinyu Wang, Ting Dai, Xingen Wang and Jin Song Dong. White-box Fairness Testing through Adversarial Sampling. 42nd International Conference on Software Engineering, Seoul, South Korea (online), Oct 2020. (ACM SIGSOFT Distinguished Paper Award, ACM SIGSOFT Research Highlights.)
The job of formal methods is to elucidate the assumptions upon which formal correctness depends - Tony Hoare
Formal methods can be incorporated throughout the development process to reduce the prevalence of multiple categories of vulnerabilities - Back to the Building Blocks
Software stack is the core driving force behind the digital operation of industrial safety-critical systems (industrial control systems, autonomous systems, etc). It is thus of paramount importance to formally verify and analyze the correctness and security of their foundational software stack, such as OS kernel, compiler, security protocol and control program, for industrial safety-critical systems. In this line of research, we are working on developing new AI-empowered logical foundations and toolkits to better model, test, verify, monitor and enforce the desired properties and behaviors for different software layers (especially those commonly used in safety-critical industries).
Related publications: [ICSE 25, WWW 25, TSE 24, AsiaCCS/CPSS 24, TSE 23, CCS 23, CONFEST/FMICS 23, FITEE 22, IoT 22, TSE 18, ICSE 18, DSN 18, STTT 18, FM 18, FASE 17, FM 16]
Sample Work:
[ICSE 2025] Ziyu Mao, Jingyi Wang*, Jun Sun, Shengchao Qin and Jiawen Xiong. LLM-aided Automatic Modelling for Security Protocol Verification. 47th International Conference on Software Engineering, Ottawa, Canada, Apr, 2025.
[WWW 2025] Xinyao Xu, Ziyu Mao, Jianzhong Su, Xingwei Lin, David Basin, Jun Sun and Jingyi Wang*. Quantitative Runtime Monitoring of Ethereum Transaction Attacks. The Web Conference, Sydney, Australia, Apr, 2025.
[TSE 2023] Kun Wang, Jingyi Wang*, Christopher M. Poskitt, Xiangxiang Chen, Jun Sun, and Peng Cheng. K-ST: A Formal Executable Semantics of the Structured Text Language for PLCs. IEEE Transactions on Software Engineering, 2023.
[TSE 2018] Jingyi Wang, Jun Sun, Shengchao Qin and Cyrille Jegourel. Automatically ‘Verifying’ Discrete-Time Complex Systems through Learning, Abstraction and Refinement, IEEE Transactions on Software Engineering, 2018.
[ICSE 2018] Xinyu Wang, Jun Sun, Zhenbang Chen, Peixin Zhang, Jingyi Wang* and Yun Lin. Towards Optimal Concolic Testing, 40th International Conference on Software Engineering, Gothenburg, Sweden, May 2018. (ACM SIGSOFT Distinguished Paper Award)