Computing a Basin of Attraction to a Target Region by Solving Bilinear Semi-Definite Problems. - Zhikun She; Bai Xue 001 (CASC, 2011)

Algebraic analysis on asymptotic stability of continuous dynamical systems. - Zhikun She; Bai Xue 001; Zhiming Zheng 001 (ISSAC, 2011)

Algebraic analysis on asymptotic stability of switched hybrid systems. - Zhikun She; Bai Xue 001 (HSCC, 2012)

Discovering polynomial Lyapunov functions for continuous dynamical systems. - Zhikun She; Haoyang Li; Bai Xue 001; Zhiming Zheng 001; Bican Xia (J. Symb. Comput., 2013)

Discovering Multiple Lyapunov Functions for Switched Hybrid Systems. - Zhikun She; Bai Xue 001 (SIAM J. Control. Optim., 2014)

Discovering multiple Lyapunov functions for switched hybrid systems with global exponential stability. - Junjie Lu; Zhikun She; Bai Xue 001 (CDC, 2015)

Under-Approximating Backward Reachable Sets by Polytopes. - Bai Xue 001; Zhikun She; Arvind Easwaran (CAV (1), 2016)

Temporal Logic Verification for Delay Differential Equations. - Peter Nazier Mosaad; Martin Fränzle; Bai Xue 001 (ICTAC, 2016)

Just scratching the surface: Partial exploration of initial values in reach-set computation. - Bai Xue 001; Martin Fränzle; Peter Nazier Mosaad (CDC, 2017)

Safe Over- and Under-Approximation of Reachable Sets for Delay Differential Equations. - Bai Xue 001; Peter Nazier Mosaad; Martin Fränzle; Mingshuai Chen; Yangjia Li; Naijun Zhan (FORMATS, 2017)

Model Checking Delay Differential Equations Against Metric Interval Temporal Logic. - Peter Nazier Mosaad; Martin Fränzle; Bai Xue 001 (Sci. Ann. Comput. Sci., 2017)

Reach-Avoid Verification for Nonlinear Systems Based on Boundary Analysis. - Bai Xue 001; Arvind Easwaran; Nam-Joon Cho; Martin Fränzle (IEEE Trans. Autom. Control., 2017)

Underapproximating Backward Reachable Sets by Semialgebraic Sets. - Bai Xue 001; Zhikun She; Arvind Easwaran (IEEE Trans. Autom. Control., 2017)

Safe Over- and Under-Approximation of Reachable Sets for Autonomous Dynamical Systems. - Meilun Li; Peter Nazier Mosaad; Martin Fränzle; Zhikun She; Bai Xue 001 (FORMATS, 2018)

Under-Approximating Reach Sets for Polynomial Continuous Systems. - Bai Xue 001; Martin Fränzle; Naijun Zhan (HSCC, 2018)

Robust Non-termination Analysis of Numerical Software. - Bai Xue 001; Naijun Zhan; Yangjia Li; Qiuye Wang (SETTA, 2018)

Robust Invariant Sets Computation for Switched Discrete-Time Polynomial Systems. - Bai Xue 001; Naijun Zhan (CoRR, 2018)

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)

Robust invariant sets generation for state-constrained perturbed polynomial systems. - Bai Xue 001; Qiuye Wang; Naijun Zhan; Martin Fränzle (HSCC, 2019)

Probably Approximate Safety Verification of Hybrid Dynamical Systems. - Bai Xue 001; Martin Fränzle; Hengjun Zhao; Naijun Zhan; Arvind Easwaran (ICFEM, 2019)

Nonlinear Craig Interpolant Generation. - Ting Gan; Bican Xia; Bai Xue 001; Naijun Zhan (CoRR, 2019)

Synthesizing More Expressive Invariants by Semidefinite Programming. - Qiuye Wang; Lihong Zhi; Naijun Zhan; Bai Xue 001; Zhi-Hong Yang (CoRR, 2019)

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

Nonlinear Craig Interpolant Generation. - Ting Gan; Bican Xia; Bai Xue 001; Naijun Zhan; Liyun Dai (CAV (1), 2020)

Inner-approximating Reach-avoid Sets for Discrete-time Polynomial Systems. - Bai Xue 001; Naijun Zhan; Martin Fränzle (CDC, 2020)

PAC Learning of Deterministic One-Clock Timed Automata. - Wei Shen; Jie An 001; Bohua Zhan; Miaomiao Zhang 003; Bai Xue 001; Naijun Zhan (ICFEM, 2020)

Probably Approximately Correct Interpolants Generation. - Bai Xue 001; Naijun Zhan (SETTA, 2020)

PRODeep: a platform for robustness verification of deep neural networks. - Renjue Li; Jianlin Li; Cheng-Chao Huang; Pengfei Yang 002; Xiaowei Huang 001; Lijun Zhang 001; Bai Xue 001; Holger Hermanns (ESEC/SIGSOFT FSE, 2020)

Inner-Approximating Reachable Sets for Polynomial Systems With Time-Varying Uncertainties. - Bai Xue 001; Martin Fränzle; Naijun Zhan (IEEE Trans. Autom. Control., 2020)

Safety Verification for Random Ordinary Differential Equations. - Bai Xue 001; Martin Fränzle; Naijun Zhan; Sergiy Bogomolov; Bican Xia (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2020)

PAC Model Checking of Black-Box Continuous-Time Dynamical Systems. - Bai Xue 001; Miaomiao Zhang 003; Arvind Easwaran; Qin Li 002 (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2020)

Reach-avoid Analysis for Stochastic Discrete-time Systems. - Bai Xue 001; Renjue Li; Naijun Zhan; Martin Fränzle (ACC, 2021)

Synthesizing Invariant Barrier Certificates via Difference-of-Convex Programming. - Qiuye Wang; Mingshuai Chen; Bai Xue 001; Naijun Zhan; Joost-Pieter Katoen (CAV (1), 2021)

Reach-Avoid Analysis for Delay Differential Equations. - Bai Xue 001; Yunjun Bai; Naijun Zhan; Wenyou Liu; Li Jiao (CDC, 2021)

Switching controller synthesis for delay hybrid systems under perturbations. - Yunjun Bai; Ting Gan; Li Jiao; Bican Xia; Bai Xue 001; Naijun Zhan (HSCC, 2021)

Brief Industry Paper: Modeling and Verification of Descent Guidance Control of Mars Lander. - Bohua Zhan; Bin Gu 006; Xiong Xu; Xiangyu Jin; Shuling Wang 003; Bai Xue 001; Xiaofeng Li; Yao Chen; Mengfei Yang; Naijun Zhan (RTAS, 2021)

Improving Neural Network Verification through Spurious Region Guided Refinement. - Pengfei Yang 002; Renjue Li; Jianlin Li; Cheng-Chao Huang; Jingyi Wang 004; Jun Sun 001; Bai Xue 001; Lijun Zhang 001 (TACAS (1), 2021)

Probabilistic Robustness Analysis for DNNs based on PAC Learning. - Renjue Li; Pengfei Yang 002; Cheng-Chao Huang; Bai Xue 001; Lijun Zhang 001 (CoRR, 2021)

Ensemble Defense with Data Diversity: Weak Correlation Implies Strong Robustness. - Renjue Li; Hanwei Zhang 001; Pengfei Yang 002; Cheng-Chao Huang; Aimin Zhou; Bai Xue 001; Lijun Zhang 001 (CoRR, 2021)

Synthesizing Robust Domains of Attraction for State-Constrained Perturbed Polynomial Systems. - Bai Xue 001; Qiuye Wang; Naijun Zhan; Shijie Wang; Zhikun She (SIAM J. Control. Optim., 2021)

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

Consensus Control for Heterogeneous Multivehicle Systems: An Iterative Learning Approach. - Shuyuan Zhang 001; Lei Wang 055; Haihui Wang; Bai Xue 001 (IEEE Trans. Neural Networks Learn. Syst., 2021)

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

Outer-approximating Controlled Reach-avoid Sets for Polynomial Systems. - Changyuan Zhao; Chuchu Fan; Bai Xue 001 (CDC, 2022)

Towards Practical Robustness Analysis for DNNs based on PAC-Model Learning. - Renjue Li; Pengfei Yang 002; Cheng-Chao Huang; Youcheng Sun; Bai Xue 001; Lijun Zhang 001 (ICSE, 2022)

Reach-Avoid Analysis for Stochastic Differential Equations. - Bai Xue 001; Naijun Zhan; Martin Fränzle (CoRR, 2022)

Encoding inductive invariants as barrier certificates: Synthesis via difference-of-convex programming. - Qiuye Wang; Mingshuai Chen; Bai Xue 001; Naijun Zhan; Joost-Pieter Katoen (Inf. Comput., 2022)

Robust Invariant Sets Computation for Discrete-Time Perturbed Nonlinear Systems. - Bai Xue 001; Naijun Zhan (IEEE Trans. Autom. Control., 2022)

Scenario Approach for Parametric Markov Models. - Ying Liu 048; Andrea Turrini; Ernst Moritz Hahn; Bai Xue 001; Lijun Zhang 001 (ATVA (1), 2023)

Safe Probabilistic Invariance Verification for Stochastic Discrete-Time Dynamical Systems. - Yiqing Yu; Taoran Wu; Bican Xia; Ji Wang 001; Bai Xue 001 (CDC, 2023)

A Geometrical Characterization on Feature Density of Image Datasets. - Zhen Liang; Changyuan Zhao; Wanwei Liu; Bai Xue 001; Wenjing Yang 002 (ICME, 2023)

Model Predictive Control with Reach-avoid Analysis. - Dejin Ren; Wanli Lu; Jidong Lv; Lijun Zhang 001; Bai Xue 001 (IJCAI, 2023)

Safety Verification for Neural Networks Based on Set-Boundary Analysis. - Zhen Liang; Dejin Ren; Wanwei Liu; Ji Wang 001; Wenjing Yang 002; Bai Xue 001 (TASE, 2023)

Provable Reach-avoid Controllers Synthesis Based on Inner-approximating Controlled Reach-avoid Sets. - Jianqiang Ding; Taoran Wu; Yuping Qian; Lijun Zhang 001; Bai Xue 001 (CoRR, 2023)

Repairing Deep Neural Networks Based on Behavior Imitation. - Zhen Liang; Taoran Wu; Changyuan Zhao; Wanwei Liu; Bai Xue 001; Wenjing Yang 002; Ji Wang 001 (CoRR, 2023)

Correct-by-Construction for Hybrid Systems by Synthesizing Reset Controller. - Jiang Liu 009; Han Su 003; Yunjun Bai; Bin Gu 006; Bai Xue 001; Mengfei Yang; Naijun Zhan (CoRR, 2023)

Stability Verification for Heterogeneous Complex Networks via Iterative SOS Programming. - Shuyuan Zhang 001; Shizhong Song; Lei Wang 055; Bai Xue 001 (IEEE Control. Syst. Lett., 2023)

Artifact for the ATVA'23 paper "Scenario Approach for Parametric Markov Models". - Ying Liu 048; Andrea Turrini; Ernst Moritz Hahn; Bai Xue 001; Lijun Zhang 001 (Zenodo, 2023)

Inner Approximating Robust Reach-Avoid Sets for Discrete-Time Polynomial Dynamical Systems. - Changyuan Zhao; Shuyuan Zhang 001; Lei Wang 055; Bai Xue 001 (IEEE Trans. Autom. Control., 2023)

Towards robust neural networks via a global and monotonically decreasing robustness training strategy. - Zhen Liang; Taoran Wu; Wanwei Liu; Bai Xue 001; Wenjing Yang 002; Ji Wang 001; Zhengbin Pang (Frontiers Inf. Technol. Electron. Eng., 2023)

Consensus verification for heterogeneous polynomial networked systems. - Shuyuan Zhang 001; Lei Wang 055; Bai Xue 001; Chanying Li; Qing-Guo Wang (J. Frankl. Inst., 2023)

An Iterative Method for Computing Controlled Reach-Avoid Sets. - Dejin Ren; Taoran Wu; Bai Xue 001 (ACC, 2024)

Reach-Avoid Analysis for Sampled-Data Systems with Measurement Uncertainties. - Taoran Wu; Dejin Ren; Shuyuan Zhang 001; Lei Wang 055; Bai Xue 001 (ACC, 2024)

Inner-Approximate Reachability Computation via Zonotopic Boundary Analysis. - Dejin Ren; Zhen Liang; Chenyu Wu; Jianqiang Ding; Taoran Wu; Bai Xue 001 (CAV (3), 2024)

PyBDR: Set-Boundary Based Reachability Analysis Toolkit in Python. - Jianqiang Ding; Taoran Wu; Zhen Liang; Bai Xue 001 (FM (2), 2024)

UR4NNV: Neural Network Verification, Under-approximation Reachability Works! - Zhen Liang; Taoran Wu; Ran Zhao; Bai Xue 001; Ji Wang 001; Wenjing Yang 002; Shaojun Deng; Wanwei Liu (CoRR, 2024)

Converse Barrier Certificates for Finite-time Safety Verification of Continuous-time Perturbed Deterministic Systems. - Yonghan Li; Chenyu Wu; Taoran Wu; Shijie Wang; Bai Xue 001 (CoRR, 2024)

A Framework for Safe Probabilistic Invariance Verification of Stochastic Dynamical Systems. - Taoran Wu; Yiqing Yu; Bican Xia; Ji Wang 001; Bai Xue 001 (CoRR, 2024)

Verifying safety of neural networks from topological perspectives. - Zhen Liang; Dejin Ren; Bai Xue 001; Ji Wang 001; Wenjing Yang 002; Wanwei Liu (Sci. Comput. Program., 2024)

Reach-Avoid Verification Based on Convex Optimization. - Bai Xue 001; Naijun Zhan; Martin Fränzle; Ji Wang 001; Wanwei Liu (IEEE Trans. Autom. Control., 2024)

Credit assignment for trained neural networks based on Koopman operator theory. - Zhen Liang; Changyuan Zhao; Wanwei Liu; Bai Xue 001; Wenjing Yang 002; Zhengbin Pang (Frontiers Comput. Sci., 2024)

Reach-Avoid Analysis for Polynomial Stochastic Differential Equations. - Bai Xue 001; Naijun Zhan; Martin Fränzle (IEEE Trans. Autom. Control., 2024)

Consensus Criterion Verification for Heterogeneous Multiagent Systems via Sum-of-Squares Programming. - Shuyuan Zhang 001; Lei Wang 055; Bai Xue 001; Deyuan Meng; Qing-Guo Wang (IEEE Trans. Autom. Control., 2024)

Qualitative and Quantitative Model Checking Against Recurrent Neural Networks. - Zhen Liang; Wan-Wei Liu; Fu Song; Bai Xue 001; Wenjing Yang 002; Ji Wang 001; Zhengbin Pang (J. Comput. Sci. Technol., 2024)

Reach-Avoid Controllers Synthesis for Safety Critical Systems. - Bai Xue 001 (IEEE Trans. Autom. Control., 2024)

Bipartite Consensus for Nonlinear Networked Systems Based on General Lyapunov Functions. - Shuyuan Zhang 001; Lei Wang 055; Bai Xue 001; Kexin Liu; Wei Wang 016 (IEEE Trans. Control. Netw. Syst., 2024)

BIRDNN: Behavior-Imitation Based Repair for Deep Neural Networks. - Zhen Liang; Taoran Wu; Changyuan Zhao; Wanwei Liu; Bai Xue 001; Wenjing Yang 002; Ji Wang 001; Wanrong Huang (Neural Networks, 2025)

Automatic Verification of Bounded Synchronization for Heterogeneous Polynomial Networked Systems. - Shuyuan Zhang 001; Lei Wang 055; Bai Xue 001; Qing-Guo Wang (IEEE Trans. Autom. Control., 2025)

Synthesizing Invariants for Polynomial Programs by Semidefinite Programming. - Hao Wu 085; Qiuye Wang; Bai Xue 001; Naijun Zhan; Lihong Zhi; Zhi-Hong Yang (ACM Trans. Program. Lang. Syst., 2025)

Convex Computations for Controlled Safety Invariant Sets of Black-box Discrete-time Dynamical Systems. - Taoran Wu; Yiling Xue; Jingduo Pan; Dejin Ren; Arvind Easwaran; Bai Xue 001 (CoRR, 2025)

Controlled Reach-avoid Set Computation for Discrete-time Polynomial Systems via Convex Optimization. - Taoran Wu; Yiling Xue; Dejin Ren; Arvind Easwaran; Martin Fränzle; Bai Xue 001 (CoRR, 2025)

Formal Modeling and Synthesis of Longitudinal Dynamics Controller for Train Platoons. - Wanli Lu; Jidong Lv; Bai Xue 001; Zhengwei Luo (IEEE Trans. Intell. Transp. Syst., 2025)