
The concept of open weak CAD is introduced. Every open CAD is an open weak
CAD. On the contrary, an open weak CAD is not necessarily an open CAD. An
algorithm for computing projection polynomials of open weak CADs is proposed.
The key idea is to compute the intersection of projection factor sets produced
by different projection orders. The resulting open weak CAD often has smaller
number of sample points than open CADs. The algorithm can be used for computing
sample points for all open connected components of $ f\neq0$ for a given
polynomial $f$. It can also be used for many other applications, such as
testing semidefiniteness of polynomials and copositive problems. In fact, we
solved several difficult semidefiniteness problems efficiently by using the
algorithm. Furthermore, applying the algorithm to copositive problems, we find
an explicit expression of the polynomials producing open weak CADs under some
conditions, which significantly improves the efficiency of solving copositive
problems.

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 a key observation that quadratic polynomial
inequalities can be linearized if they are concave. A generalization of
Motzkin's transposition theorem is proved, which is used to generate an
interpolant between two mutually contradictory conjunctions of polynomial
inequalities, using semidefinite programming in time complexity
$\mathcal{O}(n^3+nm))$, where $n$ is the number of variables and $m$ is the
number of inequalities. Using the framework proposed by \cite{SSLMCS2008} for
combining interpolants for a combination of quantifierfree theories which have
their own interpolation algorithms, a combination algorithm is given for the
combined theory of concave quadratic polynomial inequalities and the equality
theory over uninterpreted functions symbols (\textit{EUF}). The proposed
approach is applicable to all existing abstract domains like \emph{octagon},
\emph{polyhedra}, \emph{ellipsoid} and so on, therefore it can be used to
improve the scalability of existing verification techniques for programs and
hybrid systems. In addition, we also discuss how to extend our approach to
formulas beyond concave quadratic polynomials using Gr\"{o}bner basis.

A popular numerical method to compute SOS (sum of squares of polynomials)
decompositions for polynomials is to transform the problem into semidefinite
programming (SDP) problems and then solve them by SDP solvers. In this paper,
we focus on reducing the sizes of inputs to SDP solvers to improve the
efficiency and reliability of those SDP based methods. Two types of
polynomials, convex cover polynomials and split polynomials, are defined. A
convex cover polynomial or a split polynomial can be decomposed into several
smaller subpolynomials such that the original polynomial is SOS if and only if
the subpolynomials are all SOS. Thus the original SOS problem can be
decomposed equivalently into smaller subproblems. It is proved that convex
cover polynomials are split polynomials and it is quite possible that sparse
polynomials with many variables are split polynomials, which can be efficiently
detected in practice. Some necessary conditions for polynomials to be SOS are
also given, which can help refute quickly those polynomials which have no SOS
representations so that SDP solvers are not called in this case. All the new
results lead to a new SDP based method to compute SOS decompositions, which
improves this kind of methods by passing smaller inputs to SDP solvers in some
cases. Experiments show that the number of monomials obtained by our program is
often smaller than that by other SDP based software, especially for polynomials
with many variables and high degrees. Numerical results on various tests are
reported to show the performance of our program.

A new projection operator based on cylindrical algebraic decomposition (CAD)
is proposed. The new operator computes the intersection of projection factor
sets produced by different CAD projection orders. In other words, it computes
the gcd of projection polynomials in the same variables produced by different
CAD projection orders. We prove that the new operator still guarantees
obtaining at least one sample point from every connected component of the
highest dimension, and therefore, can be used for testing semidefiniteness of
polynomials. Although the complexity of the new method is still doubly
exponential, in many cases, the new operator does produce smaller projection
factor sets and fewer open cells. Some examples of testing semidefiniteness of
polynomials, which are difficult to be solved by existing tools, have been
worked out efficiently by our program based on the new method.

A barrier certificate can separate the state space of a con sidered hybrid
system (HS) into safe and unsafe parts ac cording to the safety property to be
verified. Therefore this notion has been widely used in the verification of
HSs. A stronger condition on barrier certificates means that less expressive
barrier certificates can be synthesized. On the other hand, synthesizing more
expressive barrier certificates often means high complexity. In [9], Kong et al
consid ered how to relax the condition of barrier certificates while still
keeping their convexity so that one can synthesize more expressive barrier
certificates efficiently using semidefinite programming (SDP). In this paper,
we first discuss how to relax the condition of barrier certificates in a
general way, while still keeping their convexity. Particularly, one can then
utilize different weaker conditions flexibly to synthesize dif ferent kinds of
barrier certificates with more expressiveness efficiently using SDP. These
barriers give more opportuni ties to verify the considered system. We also
show how to combine two functions together to form a combined barrier
certificate in order to prove a safety property under consid eration, whereas
neither of them can be used as a barrier certificate separately, even according
to any relaxed condi tion. Another contribution of this paper is that we
discuss how to discover certificates from the general relaxed condi tion by
SDP. In particular, we focus on how to avoid the unsoundness because of numeric
error caused by SDP with symbolic checking

Interpolationbased techniques have been widely and successfully applied in
the verification of hardware and software, e.g., in boundedmodel check ing,
CEGAR, SMT, etc., whose hardest part is how to synthesize interpolants. Various
work for discovering interpolants for propositional logic, quantifierfree
fragments of firstorder theories and their combinations have been proposed.
However, little work focuses on discovering polynomial interpolants in the
literature. In this paper, we provide an approach for constructing nonlinear
interpolants based on semidefinite programming, and show how to apply such
results to the verification of programs by examples.

This paper revisits an algorithm for isolating real roots of univariate
polynomials based on continued fractions. It follows the work of Vincent,
Uspen sky, Collins and Akritas, Johnson and Krandick. We use some tricks,
especially a new algorithm for computing an upper bound of positive roots. In
this way, the algorithm of isolating real roots is improved. The complexity of
our method for computing an upper bound of positive roots is O(n log(u+1))
where u is the optimal upper bound satisfying Theorem 3 and n is the degree of
the polynomial. Our method has been implemented as a software package logcf
using C++ language. For many benchmarks logcf is two or three times faster than
the function RootIntervals of Mathematica. And it is much faster than another
continued fractions based software CF, which seems to be one of the fastest
available open software for exact real root isolation. For those benchmarks
which have only real roots, logcf is much faster than Sleeve and eigensolve
which are based on numerical computation.

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 computing the set of all the inputs on which the
loop does not terminate. For the case of more program variables, we show that
the nontermination set cannot be described by Tarski formulae in general