15 citations · 52 across the 35 of their papers we have counts for
7 papers · 1 filter
Local Search for Solving Satisfiability of Polynomial Formulas
Haokun Li, Bican Xia, Tianqi Zhao
Satisfiability Modulo the Theory of Nonlinear Real Arithmetic, SMT(NRA) for short, concerns the satisfiability of polynomial formulas, which are quantifier-free Boolean combination…
Solving Satisfiability of Polynomial Formulas By Sample-Cell Projection
Haokun Li, Bican Xia
A new algorithm for deciding the satisfiability of polynomial formulas over the reals is proposed. The key point of the algorithm is a new projection operator, called sample-cell p…
Finding polynomial loop invariants for probabilistic programs
Yijun Feng, Lijun Zhang, David N. Jansen +2
Quantitative loop invariants are an essential element in the verification of probabilistic programs. Recently, multivariate Lagrange interpolation has been applied to synthesizing…
Interpolation synthesis for quadratic polynomial inequalities and combination with EUF
Ting Gan, Liyun Dai, Bican Xia +3
An algorithm for generating interpolants for formulas which are conjunctions of quadratic polynomial inequalities (both strict and nonstrict) is proposed. The algorithm is based on…
Generating Non-Linear Interpolants by Semidefinite Programming
Liyun Dai, Bican Xia, Naijun Zhan
Interpolation-based techniques have been widely and successfully applied in the verification of hardware and software, e.g., in bounded-model check- ing, CEGAR, SMT, etc., whose ha…
Non-Termination Sets of Simple Linear Loops
Liyun Dai, Bican Xia
A simple linear loop is a simple while loop with linear assignments and linear loop guards. If a simple linear loop has only two program variables, we give a complete algorithm for…