  Numerical tools for constraints solving are a cornerstone to control
verification problems. This is evident by the plethora of research that uses
tools like linear and convex programming for the design of control systems.
Nevertheless, the capability of linear and convex programming is limited and is
not adequate to reason about general nonlinear polynomials constraints that
arise naturally in the design of nonlinear systems. This limitation calls for
new solvers that are capable of utilizing the power of linear and convex
programming to reason about general multivariate polynomials. In this paper, we
propose PolyAR, a highly parallelizable solver for polynomial inequality
constraints. PolyAR provides several key contributions. First, it uses convex
relaxations of the problem to accelerate the process of finding a solution to
the set of the non-convex multivariate polynomials. Second, it utilizes an
iterative convex abstraction refinement process which aims to prune the search
space and identify regions for which the convex relaxation fails to solve the
problem. Third, it allows for a highly parallelizable usage of off-the-shelf
solvers to analyze the regions in which the convex relaxation failed to provide
solutions. We compared the scalability of PolyAR against Z3 8.9 and Yices 2.6
on control designing problems. Finally, we demonstrate the performance of
PolyAR on designing switching signals for continuous-time linear switching
systems.
