Selected Publications

    Optimization Based Reachability Analysis
    1. 1

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

    2. 2

      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

    3. 3

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

    4. 4

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

    5. 5

      Bai Xue. Reach-avoid Verification using Lyapunov Densities. Arxiv, 2023. PDF

    6. 6

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

    7. 7

      Bai Xue, Naijun Zhan and Martin Fränzle. Reach-Avoid Analysis for Stochastic Differential Equations. Arxiv, 2021. PDF

    8. 8

      Bai Xue, Naijun Zhan, Martin Fränzle, Ji Wang and Wanwei Liu. Reach-avoid Verification Based on Convex Optimization. To appear in IEEE Transactions on Automatic Control (IEEE TAC), 2023. Arxiv PDF

    9. 9

      Changyuan Zhao, Shuyuan Zhang, Lei Wang and Bai Xue. Inner-approximating Robust Reach-avoid Sets for Discrete-time Polynomial Dynamical Systems. To appear in IEEE Transactions on Automatic Control (IEEE TAC), 2022. PDF

    10. 10

      Changyuan Zhao, Chuchu Fan, and Bai Xue. Outer-approximating Controlled Reach-avoid Sets for Polynomial Systems. To appear in Proceedings of the 61st IEEE Conference on Decision and Control (CDC 2022), 2022. PDF

    11. 11

      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

    12. 12

      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

    13. 13

      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

      14

      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

      15

      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

      16

      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

      17

      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

      18

      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

      19

      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

      20

      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

      21

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

      22

      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). To appear in IEEE Transactions on Automatic Control (IEEE TAC), 2021. PDF

      23

      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

    Reachability Analysis Based on Propagating Set-Boundaries (Tool: PyBDR)
    1. 1

      Zhen Liang, Dejin Ren, Wanwei Liu, Ji Wang, Wenjing Yang, Bai Xue. Safety Verification for Neural Networks Based on Set-boundary Analysis. To appear in Proceedings of the 17th International Symposium on Theoretical Aspects of Software Engineering (TASE), 2023. Arxiv 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, 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)

      4

      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

      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

      7

      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

    Reachability Analysis Based on PAC Learning
    1. 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

      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

    Formal Analysis on Deep Neural Networks
    1. 1

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

    2. 2

      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

      3

      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

      4

      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

    Others
  1. 1

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

  2. 2

    Shuyuan Zhang, Shizhong Song, Lei Wang and Bai Xue. Stability Verification for Heterogeneous Complex Networks via Iterative SOS Programming. To appear in IEEE Control Systems Letters, 2022. Abstract PDF

  3. 3

    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), 2021. Abstract PDF

    1. 4

      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

      5

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

      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. To appear in Proceedings of the 27th IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS 2021), 2021. Abstract PDF

    3. 7

      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, 2021. Abstract PDF

    4. 8

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

    5. 9

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

    6. 10

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

    7. 11

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

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

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

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

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

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

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

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

      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