| 2026 | TACAS | Quantifier Elimination Meets Treewidth. | Hao Wu, Jiyu Zhu, Amir Kafshdar Goharshady, Jie An, Bican Xia, Naijun Zhan |
| 2025 | ICFEM | Avoiding Larger Conflict Regions in CDCL-Style Methods for Solving SMT-NRA. | Xinpeng Ni, Tianyi Ding, Bican Xia |
| 2024 | ATVA | Local Search for Checking Satisfiability of Formulas with Trigonometric Functions. | Xinpeng Ni, Bican Xia, Tianqi Zhao |
| 2024 | FM | On Completeness of SDP-Based Barrier Certificate Synthesis over Unbounded Domains. | Hao Wu, Shenghua Feng, Ting Gan, Jie Wang, Bican Xia, Naijun Zhan |
| 2024 | FM | Nonlinear Craig Interpolant Generation Over Unbounded Domains by Separating Semialgebraic Sets. | Hao Wu, Jie Wang, Bican Xia, Xiakun Li, Naijun Zhan, Ting Gan |
| 2024 | ISSAC | Reduction of Transcendental Decision Problems over the Reals. | Rizeng Chen, Bican Xia |
| 2023 | CAV | Local Search for Solving Satisfiability of Polynomial Formulas. | Haokun Li, Bican Xia, Tianqi Zhao |
| 2023 | ISSAC | Deciding first-order formulas involving univariate mixed trigonometric-polynomials. | Rizeng Chen, Bican Xia |
| 2023 | SETTA | Solving SMT over Non-linear Real Arithmetic via Numerical Sampling and Symbolic Verification. | Xinpeng Ni, Yulun Wu, Bican Xia |
| 2022 | ITP | Compositional Verification of Interacting Systems Using Event Monads. | Bohua Zhan, Yi Lv, Shuling Wang, Gehang Zhao, Jifeng Hao, Hong Ye, Bican Xia |
| 2021 | ISSAC | Choosing the Variable Ordering for Cylindrical Algebraic Decomposition via Exploiting Chordal Structure. | Haokun Li, Bican Xia, Huiying Zhang, Tao Zheng |
| 2020 | CAV | Nonlinear Craig Interpolant Generation. | Ting Gan, Bican Xia, Bai Xue, Naijun Zhan, Liyun Dai |
| 2019 | ISSAC | A New Sparse SOS Decomposition Algorithm Based on Term Sparsity. | Jie Wang, Haokun Li, Bican Xia |
| 2019 | ISSAC | An Effective Framework for Constructing Exponent Lattice Basis of Nonzero Algebraic Numbers. | Tao Zheng, Bican Xia |
| 2018 | AISC | Early Ending in Homotopy Path-Tracking for Real Roots. | Yu Wang, Wenyuan Wu, Bican Xia |
| 2018 | CAV | Monitoring CTMCs by Multi-clock Timed Automata. | Yijun Feng, Joost-Pieter Katoen, Haokun Li, Bican Xia, Naijun Zhan |
| 2017 | ATVA | Finding Polynomial Loop Invariants for Probabilistic Programs. | Yijun Feng, Lijun Zhang, David N. Jansen, Naijun Zhan, Bican Xia |
| 2017 | CASC | A Special Homotopy Continuation Method for a Class of Polynomial Systems. | Yu Wang, Wenyuan Wu, Bican Xia |
| 2016 | CADE | Interpolant Synthesis for Quadratic Polynomial Inequalities and Combination with EUF. | Ting Gan, Liyun Dai, Bican Xia, Naijun Zhan, Deepak Kapur, Mingshuai Chen |
| 2015 | ATVA | Decidability of the Reachability for a Family of Linear Vector Fields. | Ting Gan, Mingshuai Chen, Liyun Dai, Bican Xia, Naijun Zhan |
| 2014 | ISSAC | Constructing fewer open cells by GCD computation in CAD projection. | Jingjun Han, Liyun Dai, Bican Xia |
| 2013 | CAV | Generating Non-linear Interpolants by Semidefinite Programming. | Liyun Dai, Bican Xia, Naijun Zhan |
| 2012 | ICTAC | Non-termination Sets of Simple Linear Loops. | Liyun Dai, Bican Xia |
| 2011 | ISSAC | Computing with semi-algebraic sets represented by triangular decomposition. | Changbo Chen, James H. Davenport, Marc Moreno Maza, Bican Xia, Rong Xiao |
| 2010 | ISSAC | Triangular decomposition of semi-algebraic systems. | Changbo Chen, James H. Davenport, John P. May, Marc Moreno Maza, Bican Xia, Rong Xiao |
| 2009 | ISSAC | Computing cylindrical algebraic decomposition via triangular decomposition. | Changbo Chen, Marc Moreno Maza, Bican Xia, Lu Yang |
| 2008 | ISoLA | Program Verification by Reduction to Semi-algebraic Systems Solving. | Bican Xia, Lu Yang, Naijun Zhan |
| 2007 | ICTAC | Discovering Non-linear Ranking Functions by Solving Semi-algebraic Systems. | Yinghua Chen, Bican Xia, Lu Yang, Naijun Zhan, Chaochen Zhou |
| 2006 | AISC | Quantifier Elimination for Quartics. | Lu Yang, Bican Xia |
| 2005 | ISSAC | Stability analysis of biological systems with real solution classification. | Dongming Wang, Bican Xia |