2024
Isolating all the real roots of a mixed trigonometric-polynomial.
J. Symb. Comput., March, 2024
A decision procedure for string constraints with string/integer conversion and flat regular constraints.
Acta Informatica, March, 2024
An Algorithm for Discriminating the Complete Multiplicities of a Parametric Univariate Polynomial.
CoRR, 2024
A Framework for Safe Probabilistic Invariance Verification of Stochastic Dynamical Systems.
CoRR, 2024
OSVAuto: semi-automatic verifier for functional specifications of operating systems.
CoRR, 2024
Reduction of Transcendental Decision Problems over the Reals.
Proceedings of the 2024 International Symposium on Symbolic and Algebraic Computation, 2024
Nonlinear Craig Interpolant Generation Over Unbounded Domains by Separating Semialgebraic Sets.
Proceedings of the Formal Methods - 26th International Symposium, 2024
On Completeness of SDP-Based Barrier Certificate Synthesis over Unbounded Domains.
Proceedings of the Formal Methods - 26th International Symposium, 2024
Local Search for Checking Satisfiability of Formulas with Trigonometric Functions.
Proceedings of the Automated Technology for Verification and Analysis, 2024
2023
Square-Free Pure Triangular Decomposition of Zero-Dimensional Polynomial Systems.
J. Syst. Sci. Complex., December, 2023
Choosing better variable orderings for cylindrical algebraic decomposition via exploiting chordal structure.
J. Symb. Comput., 2023
Generalizing SDP-Based Barrier Certificate Synthesis to Unbounded Domains by Dropping Archimedean Condition.
CoRR, 2023
Isolating Bounded and Unbounded Real Roots of a Mixed Trigonometric-Polynomial.
CoRR, 2023
Solving SMT over Non-linear Real Arithmetic via Numerical Sampling and Symbolic Verification.
Proceedings of the Dependable Software Engineering. Theories, Tools, and Applications, 2023
Deciding first-order formulas involving univariate mixed trigonometric-polynomials.
Proceedings of the 2023 International Symposium on Symbolic and Algebraic Computation, 2023
Safe Probabilistic Invariance Verification for Stochastic Discrete-Time Dynamical Systems.
Proceedings of the 62nd IEEE Conference on Decision and Control, 2023
Local Search for Solving Satisfiability of Polynomial Formulas.
Proceedings of the Computer Aided Verification - 35th International Conference, 2023
2022
Square-free Strong Triangular Decomposition of Zero-dimensional Polynomial Systems.
CoRR, 2022
Compositional Verification of Interacting Systems Using Event Monads.
Proceedings of the 13th International Conference on Interactive Theorem Proving, 2022
2021
Choosing the Variable Ordering for Cylindrical Algebraic Decomposition via Exploiting Chordal Structure.
Proceedings of the ISSAC '21: International Symposium on Symbolic and Algebraic Computation, 2021
Switching controller synthesis for delay hybrid systems under perturbations.
Proceedings of the HSCC '21: 24th ACM International Conference on Hybrid Systems: Computation and Control, 2021
2020
Safety Verification for Random Ordinary Differential Equations.
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2020
Solving Satisfiability of Polynomial Formulas By Sample-Cell Projection.
CoRR, 2020
Nonlinear Craig Interpolant Generation.
Proceedings of the Computer Aided Verification - 32nd International Conference, 2020
2019
A Hybrid Procedure for Finding Real Points on a Real Algebraic Set.
J. Syst. Sci. Complex., 2019
Logcf: An Efficient Tool for Real Root Isolation.
J. Syst. Sci. Complex., 2019
Nonlinear Craig Interpolant Generation.
CoRR, 2019
An Effective Framework for Constructing Exponent Lattice Basis of Nonzero Algebraic Numbers.
Proceedings of the 2019 on International Symposium on Symbolic and Algebraic Computation, 2019
A New Sparse SOS Decomposition Algorithm Based on Term Sparsity.
Proceedings of the 2019 on International Symposium on Symbolic and Algebraic Computation, 2019
2018
Reachability Analysis for Solvable Dynamical Systems.
IEEE Trans. Autom. Control., 2018
Parameter Synthesis Problems for one parametric clock Timed Automata.
CoRR, 2018
Monitoring CTMCs by Multi-clock Timed Automata.
Proceedings of the Computer Aided Verification - 30th International Conference, 2018
Early Ending in Homotopy Path-Tracking for Real Roots.
Proceedings of the Artificial Intelligence and Symbolic Computation, 2018
2017
Open weak CAD and its applications.
J. Symb. Comput., 2017
Barrier certificates revisited.
J. Symb. Comput., 2017
Generating semi-algebraic invariants for non-autonomous polynomial hybrid systems.
J. Syst. Sci. Complex., 2017
A Special Homotopy Continuation Method for a Class of Polynomial Systems.
Proceedings of the Computer Algebra in Scientific Computing - 19th International Workshop, 2017
Finding Polynomial Loop Invariants for Probabilistic Programs.
Proceedings of the Automated Technology for Verification and Analysis, 2017
2016
Proving inequalities and solving global optimization problems via simplified CAD projection.
J. Symb. Comput., 2016
Interpolation synthesis for quadratic polynomial inequalities and combination with \textit{EUF}.
CoRR, 2016
Computing reachable sets of linear vector fields revisited.
Proceedings of the 15th European Control Conference, 2016
Interpolant Synthesis for Quadratic Polynomial Inequalities and Combination with EUF.
Proceedings of the Automated Reasoning - 8th International Joint Conference, 2016
Automated Inequality Proving and Discovering
WorldScientific, ISBN: 9789814759137, 2016
2015
Special algorithm for stability analysis of multistable biological regulatory systems.
J. Symb. Comput., 2015
Generic regular decompositions for parametric polynomial systems.
J. Syst. Sci. Complex., 2015
Smaller SDP for SOS decomposition.
J. Glob. Optim., 2015
Decidability of the Reachability for a Family of Linear Vector Fields.
Proceedings of the Automated Technology for Verification and Analysis, 2015
2014
Generic regular decompositions for generic zero-dimensional systems.
Sci. China Inf. Sci., 2014
Constructing fewer open cells by GCD computation in CAD projection.
Proceedings of the International Symposium on Symbolic and Algebraic Computation, 2014
Hierarchical Comprehensive Triangular Decomposition.
Proceedings of the Mathematical Software - ICMS 2014, 2014
2013
Discovering polynomial Lyapunov functions for continuous dynamical systems.
J. Symb. Comput., 2013
Computing with semi-algebraic sets: Relaxation techniques and effective boundaries.
J. Symb. Comput., 2013
Triangular decomposition of semi-algebraic systems.
J. Symb. Comput., 2013
Deciding Nonnegativity of Polynomials by MAPLE.
CoRR, 2013
Generating Non-linear Interpolants by Semidefinite Programming.
Proceedings of the Computer Aided Verification - 25th International Conference, 2013
2012
On Solving Parametric Polynomial Systems.
Math. Comput. Sci., 2012
logcf: An Efficient Tool for Real Root Isolation
CoRR, 2012
Non-termination Sets of Simple Linear Loops.
Proceedings of the Theoretical Aspects of Computing - ICTAC 2012, 2012
Real Root Isolation of Polynomial Equations Based on Hybrid Computation.
Proceedings of the Computer Mathematics, 2012
2011
Condition number based complexity estimate for solving polynomial systems.
J. Comput. Appl. Math., 2011
Symbolic decision procedure for termination of linear programs.
Formal Aspects Comput., 2011
Real solution isolation with multiplicity of zero-dimensional triangular systems.
Sci. China Inf. Sci., 2011
Computing the real solutions of polynomial systems with the RegularChains library in Maple.
ACM Commun. Comput. Algebra, 2011
Computing with semi-algebraic sets represented by triangular decomposition.
Proceedings of the Symbolic and Algebraic Computation, International Symposium, 2011
2010
Termination of linear programs with nonlinear constraints.
J. Symb. Comput., 2010
Recent advances in program verification through computer algebra.
Frontiers Comput. Sci. China, 2010
Zero Decomposition with Multiplicity of Zero-Dimensional Polynomial Systems
CoRR, 2010
2009
Computing cylindrical algebraic decomposition via triangular decomposition.
Proceedings of the Symbolic and Algebraic Computation, International Symposium, 2009
2008
Program Verification by Reduction to Semi-algebraic Systems Solving.
Proceedings of the Leveraging Applications of Formal Methods, 2008
2007
A New Method for Real Root Isolation of Univariate Polynomials.
Math. Comput. Sci., 2007
Solution to the Generalized Champagne Problem on simultaneous stabilization of linear systems.
Sci. China Ser. F Inf. Sci., 2007
DISCOVERER: a tool for solving semi-algebraic systems.
ACM Commun. Comput. Algebra, 2007
Discovering Non-linear Ranking Functions by Solving Semi-algebraic Systems.
Proceedings of the Theoretical Aspects of Computing, 2007
Generating Polynomial Invariants with DISCOVERER and QEPCAD.
Proceedings of the Formal Methods and Hybrid Real-Time Systems, 2007
2006
Real solution isolation using interval arithmetic.
Comput. Math. Appl., 2006
A Semi-Algebraic Approach for the Computation of Lyapunov Functions.
Proceedings of the Second IASTED International Conference on Computational Intelligence, 2006
Quantifier Elimination for Quartics.
Proceedings of the Artificial Intelligence and Symbolic Computation, 2006
2005
Program Verification by Using DISCOVERER.
Proceedings of the Verified Software: Theories, 2005
Stability analysis of biological systems with real solution classification.
Proceedings of the Symbolic and Algebraic Computation, 2005
Real Solution Classification for Parametric Semi-Algebraic Systems.
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.
J. Symb. Comput., 2002
2001
A complete algorithm for automated discovering of a class of inequality-type theorems.
Sci. China Ser. F Inf. Sci., 2001
1998
Automated Discovering and Proving for Geometric Inequalities.
Proceedings of the Automated Deduction in Geometry, 1998