Selected Publications

    Optimization (constructed via relaxing equations) Based Reachability Analysis
    1. 1

      Yonghan Li, Chenyu Wu, Taoran Wu, Shijie Wang and Bai Xue. Converse Barrier Certificates for Finite-time Safety Verification of Continuous-time Perturbed Deterministic Systems. Arxiv, 2024. PDF

    2. 2

      Dejin Ren, Taoran Wu, Bai Xue. An Iterative Method for Computing Controlled Reach-avoid sets. To appear in ACC 2024, 2024. PDF

    3. 3

      Taoran Wu, Dejin Ren, Shuyuan Zhang, Lei Wang, Bai Xue. Reach-avoid Analysis for Sampled-data Systems with Measurement Uncertainties. To appear in ACC 2024, Arxiv, 2024. PDF

    4. 4

      Bai Xue. A New Framework for Bounding Reachability Probabilities of Continuous-time Stochastic Systems. 2023. Arxiv PDF

    5. 5

      Bai Xue, Naijun Zhan and Martin Fränzle. Reach-Avoid Analysis for Polynomial Stochastic Differential Equations.IEEE Transactions on Automatic Control(IEEE TAC), 69(3): 1882--1889, 2024. Arxiv PDF

    6. 6

      Bai Xue, Naijun Zhan, Martin Fränzle, Ji Wang and Wanwei Liu. Reach-avoid Verification Based on Convex Optimization. IEEE Transactions on Automatic Control (IEEE TAC), 69(1): 598--605, 2024. Arxiv PDF

    7. 7

      Bai Xue. Safe Exit Controllers Synthesis for Continuous-time Stochastic Systems. Arxiv, 2023. PDF

    8. 8

      Yiqing Yu, Taoran Wu, Bican Xia, Ji Wang, Bai Xue. Safe Probabilistic Invariance Verification for Stochastic Discrete-time Dynamical Systems. CDC 2023, pp. 5804--5811, 2023. PDF

    9. 9

      Jianqiang Ding, Taoran Wu, Yuping Qian, Lijun Zhang, Bai Xue. Provable Reach-avoid Controllers Synthesis Based on Inner-approximating Controlled Reach-avoid Sets. Arxiv, 2023. PDF

    10. 10

      Bai Xue. Reach-avoid Controllers Synthesis for Safety Critical Systems. Arxiv, 2023. PDF

    11. 11

      Bai Xue. Reachability Verification for Stochastic Discrete-time Dynamical Systems. Arxiv, 2023. PDF

    12. 12

      Bai Xue. Reach-avoid Verification Using Lyapunov Densities. To appear in Proceedings of the 43rd Chinese Control Conference(CCC), 2024. Arxiv. PDF

    13. 13

      Dejin Ren, Wanli Lu, Jidong Lv, Lijun Zhang and Bai Xue. Model Predictive Control with Reach-Avoid Analysis.IJCAI2023, pp. 5437--5445, 2023. PDF

    14. 14

      Changyuan Zhao, Shuyuan Zhang, Lei Wang and Bai Xue. Inner-approximating Robust Reach-avoid Sets for Discrete-time Polynomial Dynamical Systems. IEEE Transactions on Automatic Control (IEEE TAC), 68(8): 4682--4694, 2023. PDF

    15. 15

      Changyuan Zhao, Chuchu Fan, and Bai Xue. Outer-approximating Controlled Reach-avoid Sets for Polynomial Systems. CDC 2022, pp. 3839--3845, 2022. PDF

    16. 16

      Bai Xue, Qiuye Wang, Naijun Zhan, Martin Fränzle and Shenghua Feng. Differential Games Based on Invariant Sets Generation. In Proceedings of the 2022 American Control Conference (ACC 2022), pp. 1285--1292, 2022. PDF

    17. 17

      Bai Xue, Yunjun Bai, Naijun Zhan, Wenyou Liu and Li Jiao. Reach-avoid Analysis for Delay Differential Equations. In Proceedings of the 2021 IEEE Conference on Decision and Control (CDC), pp. 1301-1307,2021. Abstract PDF

    18. 18

      Bai Xue, Renjue Li, Naijun Zhan and Martin Fränzle. Reach-avoid Analysis for Stochastic Discrete-time Systems. In Proceedings of the 2021 American Control Conference (ACC 2021), pp. 4879-4885, 2021. Abstract PDF

      19

      Bai Xue, Naijun Zhan and Martin Fränzle. Inner-approximating Reach-avoid Sets for Discrete-time Polynomial Systems. CDC 2020: 867--873, 2020. Abstract PDF

      20

      Bai Xue, Qiuye Wang, Naijun Zhan, Shijie Wang and Zhikun She. Synthesizing Robust Domains of Attraction for State-Constrained Perturbed Polynomial Systems. SIAM Journal on Control and Optimization (SICON), 59(2):1083--1108, 2021. Abstract PDF

      21

      Bai Xue, Martin Fränzle, Naijun Zhan, Sergiy Bogomolov and Bican Xia. Safety Verification for Random Ordinary Differential Equations. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (IEEE TCAD), 39(11): 4090-4101, 2020. (Special issue of EMSOFT 2020) PDF

      22

      Bai Xue, Naijun Zhan and Yangjia Li. Robust Regions of Attraction Generation for State-Constrained Perturbed Discrete-Time Polynomial Systems. IFAC 2020: 6405--6411, 2020. PDF

      23

      Bai Xue, Naijun Zhan and Yangjia Li. A Characterization of Robust Regions of Attraction for Discrete-Time Systems Based on Bellman Equations. IFAC 2020: 6468--6475, 2020. PDF

      24

      Bai Xue, Martin Fränzle and Naijun Zhan.Inner-Approximating Reachable Sets for Polynomial Systems with Time-Varying Uncertainties. IEEE Transactions on Automatic Control (IEEE TAC), 65(4): 1468-1483, 2020. PDF

      25

      Bai Xue, Qiuye Wang, Naijun Zhan and Martin Fränzle. Robust invariant sets generation for state-constrained perturbed polynomial systems. HSCC 2019: 128--137, 2019. PDF

      26

      Bai Xue, Martin Fräzle and Naijun Zhan. Under-Approximating Reach Sets for Polynomial Continuous Systems. HSCC 2018: 51--60, 2018. PDF

      27

      Bai Xue and Naijun Zhan. Robust Invariant Sets Computation for Discrete-Time Perturbed Nonlinear Systems (Robust Invariant Sets Computation for Switched Discrete-Time Polynomial Systems). IEEE Transactions on Automatic Control (IEEE TAC), 67(2): 1053--1060, 2022. PDF

      28

      Bai Xue, Naijun Zhan, Yangjia Li and Qiuye Wang. Robust Non-termination Analysis of Numerical Software. SETTA 2018: 69--88, 2018. (Best paper awards) PDF

    Set Boundary Propagation Based Reachability Analysis (Tool: PyBDR and BdryReach)
    1. 1

      Dejin Ren, Zhen Liang, Chenyu Wu, Jianqiang Ding, Taoran Wu and Bai Xue. Inner-approximate Reachability Computation via Zonotopic Boundary Analysis. To appear in Proceedings of the 36th International Conference on Computer Aided Verification(CAV), 2024. PDF

      2

      Zhen Liang, Dejin Ren, Bai Xue, Ji Wang, Wenjing Yang and Wanwei Liu Verifying Safety of Neural Networks from Topological Perspectives. To appear in Science of Computer Programing, 2024. PDF

      3

      Zhen Liang, Dejin Ren, Wanwei Liu, Ji Wang, Wenjing Yang, Bai Xue. Safety Verification for Neural Networks Based on Set-boundary Analysis. In Proceedings of the 17th International Symposium on Theoretical Aspects of Software Engineering (TASE), 2023. Arxiv PDF

      4

      Bai Xue, Qiuye Wang, Shenghua Feng and Naijun Zhan. Over- and Underapproximating Reach Sets for Perturbed Delay Differential Equations. IEEE Transactions on Automatic Control (IEEE TAC), 66(1): 283--290, 2021. PDF

      5

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

      6

      Bai Xue, Arvind Easwaran, Nam-Joon Cho and Martin Fränzle.Reach-Avoid Verification for Nonlinear Systems Based on Boundary Analysis. IEEE Transactions on Automatic Control (IEEE TAC), vol. 62: 3518--3523, 2017. PDF

      7

      Bai Xue, Zhikun She and Arvind Easwaran. Under-Approximating Backward Reachable Sets by Polytopes. CAV 2016: 457--476, 2016. PDF

      8

      Bai Xue, Martin Fränzle and Peter Nazier Mosaad. Just scratching the surface: Partial exploration of initial values in reach-set computation. CDC 2017: 1769--1775, 2017. PDF

      9

      Bai Xue, Zhikun She and Arvind Easwaran. Underapproximating Backward Reachable Sets by Semialgebraic Sets. IEEE Transactions on Automatic Control (IEEE TAC), 62: 5185--5197, 2017. PDF

    PAC Learning Based Reachability Analysis
    1. 1

      Renjue Li, Pengfei Yang, Cheng-Chao Huang, Youcheng Sun, Bai Xue, Lijun Zhang. Towards Practical Robustness Analysis for DNNs based on PAC-Model Learning. In Proceedings of the 44th International Conference on Software Engineering(ICSE 2022), 2022. PDF

    2. 2

      Bai Xue, Miaomiao Zhang, Arvind Easwaran and Qin Li. PAC Model Checking of Black-Box Continuous-Time Dynamical Systems. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (IEEE TCAD), 39(11): 3944--3955, 2020. (Special issue of EMSOFT 2020) PDF

      3

      Bai Xue, Yang Liu, Lei Ma, Xiyue Zhang, Meng Sun and Xiaofei Xie. Safe Inputs Approximation for Black-Box Systems. ICECCS 2019: 180--189, 2019. PDF

      4

      Bai Xue, Martin Fränzle, Hengjun Zhao, Naijun Zhan and Arvind Easwaran. Probably Approximate Safety Verification of Hybrid Dynamical Systems. ICFEM 2019: 236--252, 2019. PDF

    Others
  1. 1

    Shuyuan Zhang, Lei Wang, Bai Xue, Deyuan Meng and Qing-Guo Wang. Consensus Criterion Verification for Heterogeneous Multi-Agent Systems via Sum-of-Squares Programming.To appear in IEEE Transactions on Automatic Control(IEEE TAC), 2024. Abstract PDF

  2. 2

    Qiuye Wang, Mingshuai Chen, Bai Xue, Naijun Zhan and Joost-Pieter Katoen. Encoding inductive invariants as barrier certificates: synthesis via difference-of-convex programming.Information and Computation, 289: 104965, 2022. Abstract PDF

  3. 3

    Zhen Liang, Wanwei Liu, Fu Song, Bai Xue, Wenjing Yang, Ji Wang and Zhengbin, Pang.Qualitative and Quantitative Model Checking against Recurrent Neural Networks. Journal of Computer Science and Technology(JCST), 2023. PDF

    4

    Pengfei Yang, Renjue Li, Jianlin Li, Cheng-Chao Huang, Jingyi Wang, Jun Sun, Bai Xue and Lijun Zhang. Improving Neural Network Verification through Spurious Region Guided Refinement. In Proceedings of the 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems(TACAS 2021), 2021. PDF

    5

    Renjue Li, Jianlin Li, Cheng Huang, Pengfei Yang, Xiaowei Huang, Lijun Zhang, Bai Xue and Holger Hermanns. PRODEEP: a platform for robustness verification of deep neural networks. ESEC/FSE 2020: 1630--1634, 2020. PDF

  4. 6

    Shuyuan Zhang, Shizhong Song, Lei Wang and Bai Xue. Stability Verification for Heterogeneous Complex Networks via Iterative SOS Programming. IEEE Control Systems Letters, 7: 559-564, 2022. Abstract PDF

  5. 7

    Qiuye Wang, Mingshuai Chen, Bai Xue, Naijun Zhan and Joost-Pieter Katoen. Synthesizing Invariant Barrier Certificates via Difference-of-Convex Programming. To appear in Proceedings of the 33rd International Conference on Computer-Aided Verification(CAV 2021), pp. 443–466, 2021. Abstract PDF

    1. 8

      Shenghua Feng, Mingshuai Chen, Bai Xue, Sriram Sankaranarayanan and Naijun Zhan. Unbounded-Time Safety Verification of Stochastic Differential Dynamics. CAV 2020: 327--348, 2020. PDF

      9

      Shenghua Feng, Mingshuai Chen, Naijun Zhan, Martin Fränzle, and Bai Xue. Taming delays in dynamical systems: Unbounded verification of delay differential equations. CAV 2019: 650--669, 2019. PDF

    2. 10

      Bohua Zhan, Bin Gu, Xiong Xu, Xiangyu Jin, Shuling Wang Bai Xue, Xiaofeng Li, Yao Chen, Mengfei Yang and Naijun Zhan. Brief Industry Paper: Modeling and Verification of Descent Guidance Control of Mars Lander. In Proceedings of the 27th IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS 2021), 2021. Abstract PDF

    3. 11

      Shuyuan Zhang, Lei Wang, Haihui Wang and Bai Xue. Consensus Control for Heterogeneous Multi-vehicle Systems: An Iterative Learning Approach. To appear in [Special Issue: Adaptive Learning and Control for Autonomous Vehicles] in the IEEE Transactions on Neural Networks and Learning Systems, 32(12): 5356-5368, 2021. Abstract PDF

    4. 12

      Yunjun Bai, Ting Gan, Li Jiao, Bican Xia, Bai Xue and Naijun Zhan. Switching Controller Synthesis for Delay Hybrid Systems under Perturbations. In Proceedings of the 24th ACM International Conference on Hybrid Systems: Computation and Control(HSCC 2021), pp. 1-11, 2021. Abstract PDF

    5. 13

      Ting Gan, Bican Xia, Bai Xue, Naijun Zhan and Liyun Dai. Nonlinear Craig Interpolant Generation. CAV 2020: 415--438, 2020. Abstract PDF

    6. 14

      Bai Xue and Naijun Zhan. Probably Approximately Correct Interpolants Generation. SETTA 2020: 143--159, 2020 PDF

    7. 15

      Meilun Li, Peter Nazier Mosaad, Martin Fränzle, Zhikun She and Bai Xue. Safe Over- and Under-Approximation of Reachable Sets for Autonomous Dynamical Systems. FORMATS 2018: 252-270, 2018. PDF

    8. 16

      Wei Shen, Jie An, Bohua Zhan, Miaomiao Zhang, Bai Xue and Naijun Zhan. PAC Learning of Deterministic One-Clock Timed Automata. ICFEM 2020: 129--146, 2020. PDF

    9. 17

      Ankita Samaddar, Zahra Rahiminasab, Arvind Easwaran, Ansuman Banerjee and Bai Xue. Linearization based Safety Verification of a Glucose Control Protocol. ISORC 2019: 221--228, 2019. PDF

    10. 18

      Peter Nazier Mosaad, Martin Fränzle and Bai Xue. Model Checking Delay Differential Equations Against Metric Interval Temporal Logic. Sci. Ann. Comp. Sci., 27: 77--109, 2017. PDF

    11. 19

      Zhikun She, Bai Xue and Zhiming Zheng. Algebraic Analysis on Asymptotic Stability of Continuous Dynamical Systems. In Proceedings of the 36th International Symposium on Symbolic and Algebraic Computation (ISSAC 2011), pp. 313--320, 2011. PDF

    12. 20

      Zhikun She and Bai Xue. Algebraic Analysis on Asymptotic Stability of Switched Hybrid Systems. In Proceedings of the 15th ACM International Conference on Hybrid Systems: Computation and Control (HSCC 2012), pp. 187--196, 2012. PDF

    13. 21

      Zhikun She, Haoyang Li, Bai Xue, Zhiming Zheng, Bican Xia. Discovering polynomial Lyapunov functions for continuous dynamical systems. Journal of Symbolic Computation (JSC), 58: 41--63, 2013. PDF

    14. 22

      Zhikun She and Bai Xue. Discovering Multiple Lyapunov Functions for Switched Hybrid Systems. SIAM Journal on Control and Optimization (SICON), 52(5): 3312--3340, 2014. PDF

    15. 23

      Junjie Lu, Zhikun She and Bai Xue. Discovering multiple Lyapunov functions for switched hybrid systems with global exponential stability. In Proceedings of 2015 54th IEEE Conference on Decision and Control (CDC 2015), pp. 4252--4259, 2015. PDF