  Safety is a critical property for control systems in medicine,
transportation, manufacturing, and other applications, and can be defined as
ensuring positive invariance of a predefined safe set. This paper investigates
the problems of verifying positive invariance of a semi-algebraic set as well
as synthesizing sets that can be made positive invariant through Control
Barrier Function (CBF)-based control. The key to our approach consists of
mapping conditions for positive invariance to sum-of-squares constraints via
the Positivstellensatz from real algebraic geometry. Based on these conditions,
we propose a framework for verifying safety of CBF-based control including
single CBFs, high-order CBFs, multi-CBFs, and systems with trigonometric
dynamics and actuation constraints.
  In the area of synthesis, we propose algorithms for constructing CBFs,
namely, an alternating-descent approach and a local CBF approach. We evaluate
our approach through a case study on a linearized quadrotor model with
actuation constraints.
