I am now a Research Assistant at the Institute of Software, Chinese Academy of Sciences, Beijing, China. Prior to joining ISCAS, I worked as a Assistant Researcher at Zhongguancun Laboratory. In 2023, I received the Ph.D. degree in computer science from ISCAS under the supervision of Prof. Naijun Zhan. Check out my CV for more detailed information.

Research Interests

My primary research interests focus on the formal verification and synthesis of programs and hybrid discrete-continuous systems, aiming to enhance the reliability and effectiveness of software systems — particularly safety-critical cyber-physical systems in which physical processes and software components are deeply intertwined. The overarching goal is to advance the capabilities of formal verification techniques for complex systems and apply these developments effectively to real-world cyber-physical systems. My research topics include but are not limited to:

• Verification and Synthesis of Cyber-Physical Systems
• Probabilistic Systems
• AI for Formal Methods, Safe Learning-Enabled Systems

Publications

Book Chapter

1. Zhiyang Li, Mingqi Yang, Shenghua Feng, Mingshuai Chen (2025). Fixed-Point Reasoning for Stochastic Systems. MF’s Festschrift. To apper.

2. Shenghua Feng, Tengshun Yang, Mingshuai Chen, Naijun Zhan (2024). A Unified Framework for Quantitative Analysis of Probabilistic Programs. JPK’s Festschrift.

Conference Papers

3. Han Su, Shenghua Feng, Sinong Zhan, and Naijun Zhan (2024). Switching Controller Synthesis for Hybrid Systems Against STL Formulas. In FM 2024.
4. Hao Wu, Shenghua Feng, Ting Gan, Jie Wang, Bican Xia, Naijun Zhan (2024). On Completeness of SDP-Based Barrier Certificate Synthesis over Unbounded Domains. In FM 2024.
5. Shenghua Feng, Mingshuai Chen, Han Su, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Naijun Zhan (2023). Lower Bounds for Possibly Divergent Probabilistic Programs. Proc. ACM Program. Lang. Proc. ACM Program. Lang. (OOPSLA).
6. Bai Xue, Qiuye Wang, Naijun Zhan, Martin Fränzle, Shenghua Feng （2022. Differential Games Based on Invariant Sets Generation. In American Control Conference (ACC).
7. Bai Xue, Qiuye Wang, Shenghua Feng, Naijun Zhan (2021). Over- and Underapproximating Reach Sets for Perturbed Delay Differential Equations. In IEEE TAC 2021.
8. Shenghua Feng, Mingshuai Chen, Bai Xue, Sriram Sankaranarayanan, Naijun Zhan (2020). Unbounded-Time Safety Verification of Stochastic Differential Dynamic. In CAV 2020.
9. Shenghua Feng, Mingshuai Chen, Naijun Zhan, Martin Fränzle, and Bai Xue (2020). Taming delays in dynamical systems: Unbounded verification of delay differential equations . In CAV 2019.

Honors and Awards

• CCF Formal Methods Committee Outstanding Doctoral Dissertation, 2023.
• Outstanding Graduate of Institute of Software, CAS, 2023.

Educations

• Sep. 2018 - Jun. 2023， Ph.D. in Computer Science (with honour) at State Key Laboratory of Computer Science，Institute of Software, Chinese Academy of Sciences.
• Oct. 2019 - Apr. 2020, Visiting scholar, University of Colorado, Boulder.
• Sep. 2014 - Jun. 2018, B.Sc. in Mathematics (with honour), Nanjing University.