Automated Discovering and Proving for Geometric Inequalities. - Lu Yang; Xiaorong Hou; Bican Xia (Automated Deduction in Geometry, 1998)

A complete algorithm for automated discovering of a class of inequality-type theorems. - Lu Yang; Xiaorong Hou; Bican Xia (Sci. China Ser. F Inf. Sci., 2001)

An Algorithm for Isolating the Real Solutions of Semi-algebraic Systems. - Bican Xia; Lu Yang (J. Symb. Comput., 2002)

Real Solution Classification for Parametric Semi-Algebraic Systems. - Lu Yang; Bican Xia (Algorithmic Algebra and Logic, 2005)

Stability analysis of biological systems with real solution classification. - Dongming Wang 001; Bican Xia (ISSAC, 2005)

Program Verification by Using DISCOVERER. - Lu Yang; Naijun Zhan; Bican Xia; Chaochen Zhou (VSTTE, 2005)

Quantifier Elimination for Quartics. - Lu Yang; Bican Xia (AISC, 2006)

A Semi-Algebraic Approach for the Computation of Lyapunov Functions. - Zhikun She; Bican Xia; Rong Xiao 004 (Computational Intelligence, 2006)

Real solution isolation using interval arithmetic. - Bican Xia; Ting Zhang (Comput. Math. Appl., 2006)

Generating Polynomial Invariants with DISCOVERER and QEPCAD. - Yinghua Chen; Bican Xia; Lu Yang; Naijun Zhan (Formal Methods and Hybrid Real-Time Systems, 2007)

Discovering Non-linear Ranking Functions by Solving Semi-algebraic Systems. - Yinghua Chen; Bican Xia; Lu Yang; Naijun Zhan; Chaochen Zhou (ICTAC, 2007)

DISCOVERER: a tool for solving semi-algebraic systems. - Bican Xia (ACM Commun. Comput. Algebra, 2007)

Solution to the Generalized Champagne Problem on simultaneous stabilization of linear systems. - Qiang Guan; Long Wang 001; Bican Xia; Lu Yang; Wensheng Yu; Zhenbing Zeng (Sci. China Ser. F Inf. Sci., 2007)

A New Method for Real Root Isolation of Univariate Polynomials. - Ting Zhang; Bican Xia (Math. Comput. Sci., 2007)

Program Verification by Reduction to Semi-algebraic Systems Solving. - Bican Xia; Lu Yang; Naijun Zhan (ISoLA, 2008)

Computing cylindrical algebraic decomposition via triangular decomposition. - Changbo Chen; Marc Moreno Maza; Bican Xia; Lu Yang (ISSAC, 2009)

Zero Decomposition with Multiplicity of Zero-Dimensional Polynomial Systems - Yinglin Li; Bican Xia; Zhihai Zhang (CoRR, 2010)

Recent advances in program verification through computer algebra. - Lu Yang; Chaochen Zhou; Naijun Zhan; Bican Xia (Frontiers Comput. Sci. China, 2010)

Termination of linear programs with nonlinear constraints. - Bican Xia; Zhihai Zhang (J. Symb. Comput., 2010)

Computing with semi-algebraic sets represented by triangular decomposition. - Changbo Chen; James H. Davenport; Marc Moreno Maza; Bican Xia; Rong Xiao 004 (ISSAC, 2011)

Computing the real solutions of polynomial systems with the RegularChains library in Maple. - Changbo Chen; James H. Davenport; François Lemaire; Marc Moreno Maza; Bican Xia; Rong Xiao 004; Yuzhen Xie (ACM Commun. Comput. Algebra, 2011)

Real solution isolation with multiplicity of zero-dimensional triangular systems. - Zhihai Zhang; Tian Fang; Bican Xia (Sci. China Inf. Sci., 2011)

Symbolic decision procedure for termination of linear programs. - Bican Xia; Lu Yang; Naijun Zhan; Zhihai Zhang (Formal Aspects Comput., 2011)

Condition number based complexity estimate for solving polynomial systems. - Zhikun She; Bican Xia; Zhiming Zheng 001 (J. Comput. Appl. Math., 2011)

Real Root Isolation of Polynomial Equations Based on Hybrid Computation. - Fei Shen; Wenyuan Wu; Bican Xia (ASCM, 2012)

Non-termination Sets of Simple Linear Loops. - Liyun Dai; Bican Xia (ICTAC, 2012)

logcf: An Efficient Tool for Real Root Isolation - Liyun Dai; Bican Xia (CoRR, 2012)

On Solving Parametric Polynomial Systems. - Marc Moreno Maza; Bican Xia; Rong Xiao 004 (Math. Comput. Sci., 2012)

Generating Non-linear Interpolants by Semidefinite Programming. - Liyun Dai; Bican Xia; Naijun Zhan (CAV, 2013)

Deciding Nonnegativity of Polynomials by MAPLE. - Lu Yang; Bican Xia (CoRR, 2013)

Triangular decomposition of semi-algebraic systems. - Changbo Chen; James H. Davenport; John P. May; Marc Moreno Maza; Bican Xia; Rong Xiao 004 (J. Symb. Comput., 2013)

Computing with semi-algebraic sets: Relaxation techniques and effective boundaries. - Changbo Chen; James H. Davenport; Marc Moreno Maza; Bican Xia; Rong Xiao 004 (J. Symb. Comput., 2013)

Discovering polynomial Lyapunov functions for continuous dynamical systems. - Zhikun She; Haoyang Li; Bai Xue 001; Zhiming Zheng 001; Bican Xia (J. Symb. Comput., 2013)

Hierarchical Comprehensive Triangular Decomposition. - Zhenghong Chen; Xiaoxian Tang; Bican Xia (ICMS, 2014)

Constructing fewer open cells by GCD computation in CAD projection. - Jingjun Han; Liyun Dai; Bican Xia (ISSAC, 2014)

Generic regular decompositions for generic zero-dimensional systems. - Xiaoxian Tang; Zhenghong Chen; Bican Xia (Sci. China Inf. Sci., 2014)

Decidability of the Reachability for a Family of Linear Vector Fields. - Ting Gan; Mingshuai Chen; Liyun Dai; Bican Xia; Naijun Zhan (ATVA, 2015)

Smaller SDP for SOS decomposition. - Liyun Dai; Bican Xia (J. Glob. Optim., 2015)

Generic regular decompositions for parametric polynomial systems. - Zhenghong Chen; Xiaoxian Tang; Bican Xia (J. Syst. Sci. Complex., 2015)

Special algorithm for stability analysis of multistable biological regulatory systems. - Hoon Hong; Xiaoxian Tang; Bican Xia (J. Symb. Comput., 2015)

Automated Inequality Proving and Discovering - Bican Xia; Lu Yang (WorldScientific, 2016)

Interpolant Synthesis for Quadratic Polynomial Inequalities and Combination with EUF. - Ting Gan; Liyun Dai; Bican Xia; Naijun Zhan; Deepak Kapur; Mingshuai Chen (IJCAR, 2016)

Computing reachable sets of linear vector fields revisited. - Ting Gan; Mingshuai Chen; Yangjia Li; Bican Xia; Naijun Zhan (ECC, 2016)

Interpolation synthesis for quadratic polynomial inequalities and combination with textit{EUF}. - Ting Gan; Liyun Dai; Bican Xia; Naijun Zhan; Deepak Kapur; Mingshuai Chen (CoRR, 2016)

Proving inequalities and solving global optimization problems via simplified CAD projection. - Jingjun Han; Zhi Jin; Bican Xia (J. Symb. Comput., 2016)

Finding Polynomial Loop Invariants for Probabilistic Programs. - Yijun Feng; Lijun Zhang 001; David N. Jansen; Naijun Zhan; Bican Xia (ATVA, 2017)

A Special Homotopy Continuation Method for a Class of Polynomial Systems. - Yu Wang; Wenyuan Wu; Bican Xia (CASC, 2017)

Generating semi-algebraic invariants for non-autonomous polynomial hybrid systems. - Qiuye Wang; Yangjia Li; Bican Xia; Naijun Zhan (J. Syst. Sci. Complex., 2017)

Barrier certificates revisited. - Liyun Dai; Ting Gan; Bican Xia; Naijun Zhan (J. Symb. Comput., 2017)

Open weak CAD and its applications. - Jingjun Han; Liyun Dai; Hoon Hong; Bican Xia (J. Symb. Comput., 2017)

Early Ending in Homotopy Path-Tracking for Real Roots. - Yu Wang; Wenyuan Wu; Bican Xia (AISC, 2018)

Monitoring CTMCs by Multi-clock Timed Automata. - Yijun Feng; Joost-Pieter Katoen; Haokun Li; Bican Xia; Naijun Zhan (CAV (1), 2018)

Block SOS Decomposition. - Haokun Li; Bican Xia (CoRR, 2018)

Parameter Synthesis Problems for one parametric clock Timed Automata. - Liyun Dai; Taolue Chen 001; Zhiming Liu 001; Bican Xia; Naijun Zhan; Kim G. Larsen (CoRR, 2018)

Reachability Analysis for Solvable Dynamical Systems. - Ting Gan; Mingshuai Chen; Yangjia Li; Bican Xia; Naijun Zhan (IEEE Trans. Autom. Control., 2018)

A New Sparse SOS Decomposition Algorithm Based on Term Sparsity. - Jie Wang 037; Haokun Li; Bican Xia (ISSAC, 2019)

An Effective Framework for Constructing Exponent Lattice Basis of Nonzero Algebraic Numbers. - Tao Zheng; Bican Xia (ISSAC, 2019)

Nonlinear Craig Interpolant Generation. - Ting Gan; Bican Xia; Bai Xue 001; Naijun Zhan (CoRR, 2019)

Logcf: An Efficient Tool for Real Root Isolation. - Liyun Dai; Zhe Fan; Bican Xia; Hanwen Zhang (J. Syst. Sci. Complex., 2019)

A Hybrid Procedure for Finding Real Points on a Real Algebraic Set. - Yu Wang; Bican Xia (J. Syst. Sci. Complex., 2019)

Nonlinear Craig Interpolant Generation. - Ting Gan; Bican Xia; Bai Xue 001; Naijun Zhan; Liyun Dai (CAV (1), 2020)

Solving Satisfiability of Polynomial Formulas By Sample-Cell Projection. - Haokun Li; Bican Xia (CoRR, 2020)

Safety Verification for Random Ordinary Differential Equations. - Bai Xue 001; Martin Fränzle; Naijun Zhan; Sergiy Bogomolov; Bican Xia (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2020)

Switching controller synthesis for delay hybrid systems under perturbations. - Yunjun Bai; Ting Gan; Li Jiao; Bican Xia; Bai Xue 001; Naijun Zhan (HSCC, 2021)

Choosing the Variable Ordering for Cylindrical Algebraic Decomposition via Exploiting Chordal Structure. - Haokun Li; Bican Xia; Huiying Zhang; Tao Zheng (ISSAC, 2021)

Compositional Verification of Interacting Systems Using Event Monads. - Bohua Zhan; Yi Lv; Shuling Wang; Gehang Zhao; Jifeng Hao; Hong Ye; Bican Xia (ITP, 2022)

Square-free Strong Triangular Decomposition of Zero-dimensional Polynomial Systems. - Haokun Li; Bican Xia; Tianqi Zhao (CoRR, 2022)

Local Search for Solving Satisfiability of Polynomial Formulas. - Haokun Li; Bican Xia; Tianqi Zhao (CAV (2), 2023)

Safe Probabilistic Invariance Verification for Stochastic Discrete-Time Dynamical Systems. - Yiqing Yu; Taoran Wu; Bican Xia; Ji Wang 001; Bai Xue 001 (CDC, 2023)

Deciding first-order formulas involving univariate mixed trigonometric-polynomials. - Rizeng Chen; Bican Xia (ISSAC, 2023)

Solving SMT over Non-linear Real Arithmetic via Numerical Sampling and Symbolic Verification. - Xinpeng Ni; Yulun Wu; Bican Xia (SETTA, 2023)

Isolating Bounded and Unbounded Real Roots of a Mixed Trigonometric-Polynomial. - Rizeng Chen; Haokun Li; Bican Xia; Tianqi Zhao; Tao Zheng (CoRR, 2023)

Generalizing SDP-Based Barrier Certificate Synthesis to Unbounded Domains by Dropping Archimedean Condition. - Hao Wu 085; Shenghua Feng; Ting Gan; Jie Wang 037; Bican Xia; Naijun Zhan (CoRR, 2023)

Choosing better variable orderings for cylindrical algebraic decomposition via exploiting chordal structure. - Haokun Li; Bican Xia; Huiying Zhang; Tao Zheng (J. Symb. Comput., 2023)

Square-Free Pure Triangular Decomposition of Zero-Dimensional Polynomial Systems. - Haokun Li; Bican Xia; Tianqi Zhao (J. Syst. Sci. Complex., 2023)

Local Search for Checking Satisfiability of Formulas with Trigonometric Functions. - Xinpeng Ni; Bican Xia; Tianqi Zhao (ATVA (2), 2024)

On Completeness of SDP-Based Barrier Certificate Synthesis over Unbounded Domains. - Hao Wu 085; Shenghua Feng; Ting Gan; Jie Wang 037; Bican Xia; Naijun Zhan (FM (2), 2024)

Nonlinear Craig Interpolant Generation Over Unbounded Domains by Separating Semialgebraic Sets. - Hao Wu 085; Jie Wang 037; Bican Xia; Xiakun Li; Naijun Zhan; Ting Gan (FM (1), 2024)

Reduction of Transcendental Decision Problems over the Reals. - Rizeng Chen; Bican Xia (ISSAC, 2024)

OSVAuto: semi-automatic verifier for functional specifications of operating systems. - Yulun Wu; Bohua Zhan; Bican Xia (CoRR, 2024)

A Framework for Safe Probabilistic Invariance Verification of Stochastic Dynamical Systems. - Taoran Wu; Yiqing Yu; Bican Xia; Ji Wang 001; Bai Xue 001 (CoRR, 2024)

An Algorithm for Discriminating the Complete Multiplicities of a Parametric Univariate Polynomial. - Simin Qin; Bican Xia; Jing Yang (CoRR, 2024)

A decision procedure for string constraints with string/integer conversion and flat regular constraints. - Hao Wu 085; Yu-Fang Chen 001; Zhilin Wu; Bican Xia; Naijun Zhan (Acta Informatica, 2024)

Isolating all the real roots of a mixed trigonometric-polynomial. - Rizeng Chen; Haokun Li; Bican Xia; Tianqi Zhao; Tao Zheng (J. Symb. Comput., 2024)

A Hybrid SMT-NRA Solver: Integrating 2D Cell-Jump-Based Local Search, MCSAT and OpenCAD. - Tianyi Ding; Haokun Li; Xinpeng Ni; Bican Xia; Tianqi Zhao (CoRR, 2025)