I am now an Associate Researcher at the Institute of Software, Chinese Academy of Sciences, Beijing, China. Prior to joining ISCAS, I worked as an 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

• Shenghua Feng, Jie An, Fanjiang Xu (2026). Runtime Safety and Reach-avoid Prediction of Stochastic Systems via Observation-aware Barrier Functions. In AAAI 2026.

• Tengshun Yang*, Shenghua Feng*, Hongfei Fu, Naijun Zhan, Jingyu Ke, Shiyang Wu (2026). Piecewise Analysis of Probabilistic Programs via k-Induction. In POPL 2026.

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

• Han Su, Shenghua Feng✉, Sinong Zhan, and Naijun Zhan (2024). Switching Controller Synthesis for Hybrid Systems Against STL Formulas. In FM 2024.

• 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.

• 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).

• Bai Xue, Qiuye Wang, Naijun Zhan, Martin Fränzle, Shenghua Feng (2022). Differential Games Based on Invariant Sets Generation. In American Control Conference (ACC).

• Bai Xue, Qiuye Wang, Shenghua Feng, Naijun Zhan (2021). Over- and Underapproximating Reach Sets for Perturbed Delay Differential Equations. In IEEE TAC 2021.

• Shenghua Feng, Mingshuai Chen, Bai Xue, Sriram Sankaranarayanan, Naijun Zhan (2020). Unbounded-Time Safety Verification of Stochastic Differential Dynamic. In CAV 2020.

• Shenghua Feng, Mingshuai Chen, Naijun Zhan, Martin Fränzle, and Bai Xue (2019). 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.