Selected Publications

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

      Bai Xue. Sufficient and Necessary Barrier-like Conditions for Safety and Reach-avoid Verification of Stochastic Discrete-time Systems . Arxiv, 2024. PDF

    2. 2

      Bai Xue. Finite-time Safety and Reach-avoid Verification of Stochastic Discrete-time Systems. Arxiv, 2024. PDF

    3. 3

      Taoran Wu, Yiqing Yu, Bican Xia, Ji Wang and Bai Xue. A Framework for Safe Probabilistic Invariance Verification of Stochastic Dynamical Systems. Arxiv, 2024. PDF

    4. 4

      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

    5. 5

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

    6. 6

      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

    7. 7

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

      8. Journal
    8. 1

      Bai Xue. Reach-avoid Controllers Synthesis for Safety Critical Systems. To appear in IEEE Transactions on Automatic Control(IEEE TAC), 2024. Arxiv PDF

    9. 2

      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

    10. 3

      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

    11. 4

      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

      12. 5

      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

      6

      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

      7

      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

      8

      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

      Conference
    12. 1

      Bai Xue. Safe Exit Controllers Synthesis for Continuous-time Stochastic Systems. Arxiv, to appear in CDC 2024, 2024. PDF

    13. 2

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

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

    15. 4

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

    16. 5

      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

    17. 6

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

    18. 7

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

    19. 8

      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

    20. 9

      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

    21. 10

      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

      11

      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

      12

      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

      13

      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

      14

      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

      15

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

      16

      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. Journal
      1

      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

      2

      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

      3

      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

      4

      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

      Conference
      1

      Jianqiang Ding, Taoran Wu, Zhen Liang and Bai Xue. PyBDR: Set-boundary based Reachability Analysis Toolkit in Python. To appear in Proceedings of the 26th International Symposium on Formal Methods(FM), 2024. PDF

      2

      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

      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, 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)

      5

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

      6

      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

    PAC Learning Based Reachability Analysis
    1. Journal
      1

      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

      Conference
      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

      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

      3

      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, and Qing-Guo Wang. Automatic Verification of Bounded Synchronization for Heterogeneous Polynomial Networked Systems.To appear in IEEE Transactions on Automatic Control(IEEE TAC), 2024. Abstract PDF

  2. 2

    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

  3. 3

    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

  4. 4

    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

    5

    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

    6

    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

  5. 7

    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

  6. 8

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

      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

      10

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

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

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

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

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

    6. 15

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

    7. 16

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

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

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

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

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

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

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

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

      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