
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.

We extend a templatebased approach for synthesizing switching controllers
for semialgebraic hybrid systems, in which all expressions are polynomials.
This is achieved by combining a QE (quantifier elimination)based method for
generating continuous invariants with a qualitative approach for predefining
templates. Our synthesis method is relatively complete with regard to a given
family of predefined templates. Using qualitative analysis, we discuss
heuristics to reduce the numbers of parameters appearing in the templates. To
avoid too much human interaction in choosing templates as well as the high
computational complexity caused by QE, we further investigate applications of
the SOS (sumofsquares) relaxation approach and the template polyhedra
approach in continuous invariant generation, which are both well supported by
efficient numerical solvers.

In this paper, we propose an approach to reduce the optimal controller
synthesis problem of hybrid systems to quantifier elimination; furthermore, we
also show how to combine quantifier elimination with numerical computation in
order to make it more scalable but at the same time, keep arising errors due to
discretization manageable and within bounds. A major advantage of our approach
is not only that it avoids errors due to numerical computation, but it also
gives a better optimal controller. In order to illustrate our approach, we use
the real industrial example of an oil pump provided by the German company HYDAC
within the European project Quasimodo as a case study throughout this paper,
and show that our method improves (up to 7.5%) the results reported in [3]
based on game theory and model checking.

Modular exponentiation is a common mathematical operation in modern
cryptography. This, along with modular multiplication at the base and exponent
levels (to different moduli) plays an important role in a large number of key
agreement protocols. In our earlier work, we gave many decidability as well as
undecidability results for multiple equational theories, involving various
properties of modular exponentiation. Here, we consider a partial subtheory
focussing only on exponentiation and multiplication operators. Two main results
are proved. The first result is positive, namely, that the unification problem
for the above theory (in which no additional property is assumed of the
multiplication operators) is decidable. The second result is negative: if we
assume that the two multiplication operators belong to two different abelian
groups, then the unification problem becomes undecidable.