电子邮件： wangsl@ios.ac.cn
通信地址： 北京市中关村南四街4号中科院软件园区5号楼332室
邮政编码：
研究领域
AI赋能的软件形式化与验证，大模型增强的智能模型驱动设计与开发，安全攸关系统的可信保障
招生信息
课题组招收大二、大三本科生参与前沿科研，如对AI赋能的软件形式化与验证等方向有浓厚兴趣，请将个人简历发送至本人邮箱wangsl@ios.ac.cn。
招生专业
招生方向
教育背景
工作经历
工作简历
出版信息
发表著作
发表论文
1.Yuzhen Qi, Shuling Wang*, Xiangyu Jin, Xiong Xu, and Naijun Zhan (2026): Verified Numerical Semantics and Code Extraction for Simulink. IEEE TCAD 2026 (accepted by EMSOFT 2026, special issue of ESWEEK 2026).
2.Xiong Xu, Shuling Wang*, Bohua Zhan, Binghao Mu, Xiangyu Jin, Guanhua Lin, Xing Li, Fanjiang Xu, Bin Gu, Mengfei Yang, Naijun Zhan，MARS 2.0: A Toolchain for Designing Safety-Critical Cyber-Physical Systems, ACM Transactions on Embedded Computing Systems, 2026.
3.Fanpeng Yang, Xing Li, Shuling Wang, Jie An, Zeyu Sun, Shenghua Feng, Wenhan Wang, Weiyi Wang, Naijun Zhan, Fanjiang Xu (2026): How Powerful are LLMs in Generating Program Specifications? In the Proceedings of ICML 2026.
4. Yuzhen Qi, Shuling Wang*, Xing Li, Bohua Zhan, Naijun Zhan (2026): Formal semantics for hierarchical Simulink diagrams in Isabelle/HOL. Journal of Systems Architecture, 174: 103724, 2026
5.Yihao Yin, Hao Wu, Wan Liu, Shuling Wang*, Xiong Xu, Wang Lin, Fanjiang Xu, Naijun Zhan (2026): Formal design of safety-critical systems with MARS. Journal of Systems Architecture, 174:103711.
6.Xiong Xu, Ehsan Ahmad, Shuling Wang*, Xiangyu Jin, Bohua Zhan, and Naijun Zhan (2025): Modeling and Verification of Hybrid Systems by Extending AADL. ACM Transactions on Software Engineering and Methodology, 35(3):1-51.
7. Xiong Xu, Jean-Pierre Talpin, Shuling Wang, Hao Wu, Bohua Zhan, Xinxin Liu, Naijun Zhan, HpC: A Calculus for Hybrid and Mobile Systems,Proceedings of the ACM on Programming Languages, Volume 9, Issue OOPSLA1,Article No.: 121, Pages 1158 - 1183 (2025)
8. Shuling Wang, Zekun Ji, Xiong Xu, Bohua Zhan, Qiang Gao and Naijun Zhan. Formally
Verified C Code Generation from Hybrid Communicating Sequential Processes, accepted for
ICCPS 2024
9. Xiong Xu, Shuling Wang, Bohua Zhan, Xiangyu Jin, Naijun Zhan, Jean-Pierre Talpin,
Unified Graphical Co-modelling, Analysis and Verification of Cyber-physical Systems by
Combining AADL and Simulink/Stateflow, Theoretical Computer Science, 903：1-25, 2023
10. Zekun Ji, Shuling Wang*, Xiong Xu. Session Types with Multiple Senders Single Receiver,
SETTA 2023
11. Xiong Xu, Jean-Pierre Talpin, Shuling Wang, Bohua Zhan, Naijun Zhan. Semantics
Foundation for Cyber-Physical Systems Using Higher-Order UTP, ACM Transactions on
Software Engineering and Methodology, 32(1), 2022
12. Tengshun Yang, Shuling Wang, Bohua Zhan, Naijun Zhan, Jinghui Li, Shuangqing Xiang,
Zhan Xiang, Bifei Mao. Formal Analysis of 5G Authentication and Key Management for
Applications (AKMA), Journal of Systems Architecture, 126：102478, 2022
13. Panhua Guo, Bohua Zhan, Xiong Xu, Shuling Wang, Wenhui Sun. Translating a large subset
of stateflow to hybrid CSP with code optimization, Journal of Systems Architecture, 130：
102665, 2022
14. Bohua Zhan, Yi Lv, Shuling Wang, Gehang Zhao, Jifeng Hao, Hong Ye, Bican Xia.
Compositional Verification of Interacting Systems Using Event Monads, ITP 2022, 2022
15. Shicheng Yi, Shuling Wang*, Bohua Zhan, Naijun Zhan. Machine-Checked Executable
Semantics of Stateflow, ICFEM 2022: Formal Methods and Software Engineering, Madrid,
Spain, 2022
16. Bohua Zhan, Bin Gu, Xiong Xu, Xiangyu Jin, Shuling Wang, Bai Xue, Xiaofeng Li, Yao
Chen, Mengfei Yang, Naijun Zhan. Brief Industry Paper: Modeling and Verification of
Descent Guidance Control of Mars Lander, IEEE RTAS, 2021
17. Gaogao Yan, Li Jiao, Shuling Wang, Lingtai Wang, Naijun Zhan。Automatically Generating
SystemC Code from HCSP Formal Models. ACM Trans. Softw. Eng. Methodol. 29(1):
4:1-4:39, 2020
18. Lin Qianqian, Wang Shuling, Zhan Bohua, Gu Bin. Modelling and Verification of Real-Time
Publish and Subscribe Protocol Using UPPAAL and Simulink/Stateflow, Journal of Computer
Science and Technology, 35(6), pp. 1324-1342, 2020
19. Junyi Liu, Bohua Zhan*, Shuling Wang*, Shenggang Ying, Tao Liu, Yangjia Li, Mingsheng
Ying and Naijun Zhan (2019): Formal verification of quantum algorithms using quantum Hoare logic. In Proc. of CAV 2019
20. Shuling Wang*, Flemming Nielson, Hanne Riis Nielson, Naijun Zhan, Modelling and
Verifying Communication Failure of Hybrid Systems in HCSP. The Computer Journal 60(8),
pp. 1111-1130
21. Shuling Wang*, Naijun Zhan, Lijun Zhang, A Compositional Modelling and Verification
Framework for Stochastic Hybrid Systems, Formal Aspects of Computing. Volume 29, Issue
4, pp 751–775, 2017.
22. Gaogao Yan, Li Jiao, Shuling Wang* and Naijun Zhan (2017): Generating SystemC code
from delay HCSP. In Proc. of APLAS 2017, LNCS 10695, pp.21-41. 2017.
23. Gaogao Yan, Li Jiao, Yangjia Li, Shuling Wang*, Naijun Zhan* (2016): Approximate
bisimulation and discretization of Hybrid CSP. 21st International Symposium on Formal
Methods (FM 2016), LNCS 9995, pp.702-720. Limassol, 2016.
24. Shuling Wang*, Naijun Zhan, and Liang Zou: An Improved HHL Prover: An Interactive
Theorem Prover for Hybrid Systems. The 17th International Conference on Formal
Engineering Methods (ICFEM 2015), LNCS 9407, pp. 382-399, 2015.
25. Liang Zou, Naijun Zhan, Shuling Wang*, Martin Fränzle: Formal Verification of
Simulink/Stateflow Diagrams. 13th International Symposium on Automated Technology for
Verification and Analysis (ATVA 2015), LNCS 9346, pp. 464-481, 2015.
26. Shuling Wang*, Flemming Nielson, Hanne Riis Nielson, Denial of Service Security Attack
in the Continuous-Time World, 34th IFIP International Conference on Formal Techniques for
Distributed Objects, Components and Systems (FORTE 2014), LNCS 8461, pp. 149–165,
2014.
27. Liang Zou, Naijun Zhan, Shuling Wang, Martin Fraenzle, and Shengchao Qin. Verifying
Simulink Diagrams via a Hybrid Hoare Logic Prover. International Conference on Embedded
Software (EMSOFT'13), pp. 1-10, Montreal, Canada. The ACM Press. 2013.
指导学生
已指导学生
易士程 硕士研究生 081200-计算机科学与技术
计泽坤 硕士研究生 081200-计算机科学与技术
现指导学生
徐家乐 硕士研究生 081200-计算机科学与技术
马旭 硕士研究生 085405-软件工程
戚玉振 硕士研究生 083500-软件工程
杨范芃 硕士研究生 081200-计算机科学与技术
李星 硕士研究生 085405-软件工程