Selected Publications

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

      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

      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

    Reachability Analysis Based on Quantified Constraint Solving
    1. Bai Xue, Naijun Zhan and Martin Fränzle. Reach-Avoid Analysis for Stochastic Differential Equations. Arxiv, 2021. PDF

      Bai Xue, Naijun Zhan, Martin Fränzle, Ji Wang and Wanwei Liu. Reach-avoid Verification Based on Convex Optimization. Arxiv, 2022. PDF

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

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

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

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

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

      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

      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

      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

      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

      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

      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

      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

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

      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

      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 (PyBDR: a prototype tool in Python)
    1. 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

      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)

      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

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

      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

      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

    Formal Analysis on Deep Neural Networks
    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

      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

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

      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. 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. 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. 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. Ting Gan, Bican Xia, Bai Xue, Naijun Zhan and Liyun Dai. Nonlinear Craig Interpolant Generation. CAV 2020: 415--438, 2020. Abstract PDF

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

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