Over- and Under-Approximating Reachable Sets for Perturbed Delay Differential Equations. - Bai Xue 001; Qiuye Wang; Shenghua Feng; Naijun Zhan (CoRR, 2018)

Taming Delays in Dynamical Systems - Unbounded Verification of Delay Differential Equations. - Shenghua Feng; Mingshuai Chen; Naijun Zhan; Martin Fränzle; Bai Xue 001 (CAV (1), 2019)

Unbounded-Time Safety Verification of Stochastic Differential Dynamics. - Shenghua Feng; Mingshuai Chen; Bai Xue 001; Sriram Sankaranarayanan 001; Naijun Zhan (CAV (2), 2020)

Over- and Underapproximating Reach Sets for Perturbed Delay Differential Equations. - Bai Xue 001; Qiuye Wang; Shenghua Feng; Naijun Zhan (IEEE Trans. Autom. Control., 2021)

Differential Games Based on Invariant Sets Generation. - Bai Xue 001; Qiuye Wang; Naijun Zhan; Martin Fränzle; Shenghua Feng (ACC, 2022)

Reset Controller Synthesis by Reach-avoid Analysis for Delay Hybrid Systems. - Han Su 003; Jiyu Zhu; Shenghua Feng; Yunjun Bai; Bin Gu 006; Jiang Liu 009; Mengfei Yang; Naijun Zhan (CoRR, 2023)

Generalizing SDP-Based Barrier Certificate Synthesis to Unbounded Domains by Dropping Archimedean Condition. - Hao Wu 085; Shenghua Feng; Ting Gan; Jie Wang 037; Bican Xia; Naijun Zhan (CoRR, 2023)

Lower Bounds for Possibly Divergent Probabilistic Programs. - Shenghua Feng; Mingshuai Chen; Han Su 003; Benjamin Lucien Kaminski; Joost-Pieter Katoen; Naijun Zhan (Proc. ACM Program. Lang., 2023)

A Unified Framework for Quantitative Analysis of Probabilistic Programs. - Shenghua Feng; Tengshun Yang; Mingshuai Chen; Naijun Zhan (Principles of Verification (1), 2024)

Switching Controller Synthesis for Hybrid Systems Against STL Formulas. - Han Su 003; Shenghua Feng; Sinong Zhan; Naijun Zhan (FM (2), 2024)

On Completeness of SDP-Based Barrier Certificate Synthesis over Unbounded Domains. - Hao Wu 085; Shenghua Feng; Ting Gan; Jie Wang 037; Bican Xia; Naijun Zhan (FM (2), 2024)