Bican Xia

CoRR, 2024

Reduction of Transcendental Decision Problems over the Reals.

[BibT_eX]

[DOI]

Rizeng Chen

Proceedings of the 2024 International Symposium on Symbolic and Algebraic Computation, 2024

Nonlinear Craig Interpolant Generation Over Unbounded Domains by Separating Semialgebraic Sets.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods - 26th International Symposium, 2024

On Completeness of SDP-Based Barrier Certificate Synthesis over Unbounded Domains.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods - 26th International Symposium, 2024

2023

Square-Free Pure Triangular Decomposition of Zero-Dimensional Polynomial Systems.

[BibT_eX]

[DOI]

Tianqi Zhao

J. Syst. Sci. Complex., December, 2023

Choosing better variable orderings for cylindrical algebraic decomposition via exploiting chordal structure.

[BibT_eX]

[DOI]

J. Symb. Comput., 2023

Generalizing SDP-Based Barrier Certificate Synthesis to Unbounded Domains by Dropping Archimedean Condition.

[BibT_eX]

[DOI]

CoRR, 2023

Isolating Bounded and Unbounded Real Roots of a Mixed Trigonometric-Polynomial.

[BibT_eX]

[DOI]

CoRR, 2023

Solving SMT over Non-linear Real Arithmetic via Numerical Sampling and Symbolic Verification.

[BibT_eX]

[DOI]

Xinpeng Ni

Yulun Wu

Proceedings of the Dependable Software Engineering. Theories, Tools, and Applications, 2023

Deciding first-order formulas involving univariate mixed trigonometric-polynomials.

[BibT_eX]

[DOI]

Rizeng Chen

Proceedings of the 2023 International Symposium on Symbolic and Algebraic Computation, 2023

Safe Probabilistic Invariance Verification for Stochastic Discrete-Time Dynamical Systems.

[BibT_eX]

[DOI]

Proceedings of the 62nd IEEE Conference on Decision and Control, 2023

Local Search for Solving Satisfiability of Polynomial Formulas.

[BibT_eX]

[DOI]

Tianqi Zhao

Proceedings of the Computer Aided Verification - 35th International Conference, 2023

2022

Square-free Strong Triangular Decomposition of Zero-dimensional Polynomial Systems.

[BibT_eX]

[DOI]

Tianqi Zhao

CoRR, 2022

Compositional Verification of Interacting Systems Using Event Monads.

[BibT_eX]

[DOI]

Proceedings of the 13th International Conference on Interactive Theorem Proving, 2022

2021

Choosing the Variable Ordering for Cylindrical Algebraic Decomposition via Exploiting Chordal Structure.

[BibT_eX]

[DOI]

Proceedings of the ISSAC '21: International Symposium on Symbolic and Algebraic Computation, 2021

Switching controller synthesis for delay hybrid systems under perturbations.

[BibT_eX]

[DOI]

Proceedings of the HSCC '21: 24th ACM International Conference on Hybrid Systems: Computation and Control, 2021

2020

Safety Verification for Random Ordinary Differential Equations.

[BibT_eX]

[DOI]

IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2020

Solving Satisfiability of Polynomial Formulas By Sample-Cell Projection.

[BibT_eX]

[DOI]

CoRR, 2020

Nonlinear Craig Interpolant Generation.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 32nd International Conference, 2020

2019

A Hybrid Procedure for Finding Real Points on a Real Algebraic Set.

[BibT_eX]

[DOI]

Yu Wang

J. Syst. Sci. Complex., 2019

Logcf: An Efficient Tool for Real Root Isolation.

[BibT_eX]

[DOI]

J. Syst. Sci. Complex., 2019

Nonlinear Craig Interpolant Generation.

[BibT_eX]

[DOI]

CoRR, 2019

An Effective Framework for Constructing Exponent Lattice Basis of Nonzero Algebraic Numbers.

[BibT_eX]

[DOI]

Tao Zheng

Proceedings of the 2019 on International Symposium on Symbolic and Algebraic Computation, 2019

A New Sparse SOS Decomposition Algorithm Based on Term Sparsity.

[BibT_eX]

[DOI]

Jie Wang

Proceedings of the 2019 on International Symposium on Symbolic and Algebraic Computation, 2019

2018

Reachability Analysis for Solvable Dynamical Systems.

[BibT_eX]

[DOI]

IEEE Trans. Autom. Control., 2018

Parameter Synthesis Problems for one parametric clock Timed Automata.

[BibT_eX]

[DOI]

CoRR, 2018

Block SOS Decomposition.

[BibT_eX]

[DOI]

CoRR, 2018

Monitoring CTMCs by Multi-clock Timed Automata.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 30th International Conference, 2018

Early Ending in Homotopy Path-Tracking for Real Roots.

[BibT_eX]

[DOI]

Yu Wang

Wenyuan Wu

Proceedings of the Artificial Intelligence and Symbolic Computation, 2018

2017

Open weak CAD and its applications.

[BibT_eX]

[DOI]

J. Symb. Comput., 2017

Barrier certificates revisited.

[BibT_eX]

[DOI]

J. Symb. Comput., 2017

Generating semi-algebraic invariants for non-autonomous polynomial hybrid systems.

[BibT_eX]

[DOI]

J. Syst. Sci. Complex., 2017

A Special Homotopy Continuation Method for a Class of Polynomial Systems.

[BibT_eX]

[DOI]

Yu Wang

Wenyuan Wu

Proceedings of the Computer Algebra in Scientific Computing - 19th International Workshop, 2017

Finding Polynomial Loop Invariants for Probabilistic Programs.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2017

2016

Proving inequalities and solving global optimization problems via simplified CAD projection.

[BibT_eX]

[DOI]

Jingjun Han

Zhi Jin

J. Symb. Comput., 2016

Interpolation synthesis for quadratic polynomial inequalities and combination with \textit{EUF}.

[BibT_eX]

[DOI]

CoRR, 2016

Computing reachable sets of linear vector fields revisited.

[BibT_eX]

[DOI]

Proceedings of the 15th European Control Conference, 2016

Interpolant Synthesis for Quadratic Polynomial Inequalities and Combination with EUF.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning - 8th International Joint Conference, 2016

Automated Inequality Proving and Discovering

[BibT_eX]

[DOI]

WorldScientific, ISBN: 9789814759137, 2016

2015

Special algorithm for stability analysis of multistable biological regulatory systems.

[BibT_eX]

[DOI]

Hoon Hong

J. Symb. Comput., 2015

Generic regular decompositions for parametric polynomial systems.

[BibT_eX]

[DOI]

Zhenghong Chen

J. Syst. Sci. Complex., 2015

Smaller SDP for SOS decomposition.

[BibT_eX]

[DOI]

J. Glob. Optim., 2015

Decidability of the Reachability for a Family of Linear Vector Fields.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2015

2014

Generic regular decompositions for generic zero-dimensional systems.

[BibT_eX]

[DOI]

Zhenghong Chen

Sci. China Inf. Sci., 2014

Constructing fewer open cells by GCD computation in CAD projection.

[BibT_eX]

[DOI]

Jingjun Han

Proceedings of the International Symposium on Symbolic and Algebraic Computation, 2014

Hierarchical Comprehensive Triangular Decomposition.

[BibT_eX]

[DOI]

Zhenghong Chen

Proceedings of the Mathematical Software - ICMS 2014, 2014

2013

Discovering polynomial Lyapunov functions for continuous dynamical systems.

[BibT_eX]

[DOI]

J. Symb. Comput., 2013

Computing with semi-algebraic sets: Relaxation techniques and effective boundaries.

[BibT_eX]

[DOI]

J. Symb. Comput., 2013

Triangular decomposition of semi-algebraic systems.

[BibT_eX]

[DOI]

J. Symb. Comput., 2013

Deciding Nonnegativity of Polynomials by MAPLE.

[BibT_eX]

[DOI]

CoRR, 2013

Generating Non-linear Interpolants by Semidefinite Programming.

[BibT_eX]

[DOI]

Naijun Zhan

Proceedings of the Computer Aided Verification - 25th International Conference, 2013

2012

On Solving Parametric Polynomial Systems.

[BibT_eX]

[DOI]

Marc Moreno Maza

Rong Xiao

Math. Comput. Sci., 2012

logcf: An Efficient Tool for Real Root Isolation

[BibT_eX]

[DOI]

CoRR, 2012

Non-termination Sets of Simple Linear Loops.

[BibT_eX]

[DOI]

Proceedings of the Theoretical Aspects of Computing - ICTAC 2012, 2012

Real Root Isolation of Polynomial Equations Based on Hybrid Computation.

[BibT_eX]

[DOI]

Fei Shen

Wenyuan Wu

Proceedings of the Computer Mathematics, 2012

2011

Condition number based complexity estimate for solving polynomial systems.

[BibT_eX]

[DOI]

Zhikun She

Zhiming Zheng

J. Comput. Appl. Math., 2011

Symbolic decision procedure for termination of linear programs.

[BibT_eX]

[DOI]

Formal Aspects Comput., 2011

Real solution isolation with multiplicity of zero-dimensional triangular systems.

[BibT_eX]

[DOI]

Zhihai Zhang

Tian Fang

Sci. China Inf. Sci., 2011

Computing the real solutions of polynomial systems with the RegularChains library in Maple.

[BibT_eX]

[DOI]

ACM Commun. Comput. Algebra, 2011

Computing with semi-algebraic sets represented by triangular decomposition.

[BibT_eX]

[DOI]

Proceedings of the Symbolic and Algebraic Computation, International Symposium, 2011

2010

Termination of linear programs with nonlinear constraints.

[BibT_eX]

[DOI]

Zhihai Zhang

J. Symb. Comput., 2010

Recent advances in program verification through computer algebra.

[BibT_eX]

[DOI]

Frontiers Comput. Sci. China, 2010

Zero Decomposition with Multiplicity of Zero-Dimensional Polynomial Systems

[BibT_eX]

[DOI]

Yinglin Li

Zhihai Zhang

CoRR, 2010

2009

Computing cylindrical algebraic decomposition via triangular decomposition.

[BibT_eX]

[DOI]

Proceedings of the Symbolic and Algebraic Computation, International Symposium, 2009

2008

Program Verification by Reduction to Semi-algebraic Systems Solving.

[BibT_eX]

[DOI]

Naijun Zhan

Proceedings of the Leveraging Applications of Formal Methods, 2008

2007

A New Method for Real Root Isolation of Univariate Polynomials.

[BibT_eX]

[DOI]

Ting Zhang

Math. Comput. Sci., 2007

Solution to the Generalized Champagne Problem on simultaneous stabilization of linear systems.

[BibT_eX]

[DOI]

Sci. China Ser. F Inf. Sci., 2007

DISCOVERER: a tool for solving semi-algebraic systems.

[BibT_eX]

[DOI]

ACM Commun. Comput. Algebra, 2007

Discovering Non-linear Ranking Functions by Solving Semi-algebraic Systems.

[BibT_eX]

[DOI]

Proceedings of the Theoretical Aspects of Computing, 2007

Generating Polynomial Invariants with DISCOVERER and QEPCAD.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods and Hybrid Real-Time Systems, 2007

2006

Real solution isolation using interval arithmetic.

[BibT_eX]

[DOI]

Ting Zhang

Comput. Math. Appl., 2006

A Semi-Algebraic Approach for the Computation of Lyapunov Functions.

[BibT_eX]

Zhikun She

Rong Xiao

Proceedings of the Second IASTED International Conference on Computational Intelligence, 2006

Quantifier Elimination for Quartics.

[BibT_eX]

[DOI]

Proceedings of the Artificial Intelligence and Symbolic Computation, 2006

2005

Program Verification by Using DISCOVERER.

[BibT_eX]

[DOI]

Proceedings of the Verified Software: Theories, 2005

Stability analysis of biological systems with real solution classification.

[BibT_eX]

[DOI]

Dongming Wang

Proceedings of the Symbolic and Algebraic Computation, 2005

Real Solution Classification for Parametric Semi-Algebraic Systems.

[BibT_eX]

Proceedings of the Algorithmic Algebra and Logic. Proceedings of the A3L 2005, 2005

2002

An Algorithm for Isolating the Real Solutions of Semi-algebraic Systems.

[BibT_eX]

[DOI]

J. Symb. Comput., 2002

2001

A complete algorithm for automated discovering of a class of inequality-type theorems.

[BibT_eX]

[DOI]

Xiaorong Hou

Sci. China Ser. F Inf. Sci., 2001

1998

Automated Discovering and Proving for Geometric Inequalities.

[BibT_eX]

[DOI]

Xiaorong Hou