  The design of cyber-physical systems is challenging in that it includes the
analysis and synthesis of distributed and embedded real-time systems for
controlling, often in a nonlinear way, the environment. We address this
challenge with EFSMT, the exists-forall quantified first-order fragment of
propositional combinations over constraints (including nonlinear arithmetic),
as the logical framework and foundation for analyzing and synthesizing
cyber-physical systems. We demonstrate the expressiveness of EFSMT by reducing
a number of pivotal verification and synthesis problems to EFSMT. Exemplary
problems in this paper include synthesis for robust control via BIBO stability,
Lyapunov coefficient finding for nonlinear control systems, distributed
priority synthesis for orchestrating system components, and synthesis for
hybrid control systems. We are also proposing an algorithm for solving EFSMT
problems based on the interplay between two SMT solvers for respectively
solving universally and existentially quantified problems. This algorithms
builds on commonly used techniques in modern SMT solvers, and generalizes them
to quantifier reasoning by counterexample-guided constraint strengthening. The
EFSMT solver uses Bernstein polynomials for solving nonlinear arithmetic
constraints.
