# A Semi-Algebraic Framework for Verification and Synthesis of Control Barrier Functions

arXiv: https://arxiv.org/abs/2209.00081 · HTML: https://mlsanity.com/paper/2209.00081/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 31 Aug 2022.

## Built on by (most cited first, 3 of 3)

- [Bridging Control with Neural Network Verifier alpha-beta-CROWN: A Tutorial](https://mlsanity.com/paper/2605.26577/) (2026)
- [Provably Safe, Yet Scalable Reinforcement Learning](https://mlsanity.com/paper/2606.14536/) (2026)
- [Fault Tolerant Neural Control Barrier Functions for Robotic Systems under Sensor Faults and Attacks](https://mlsanity.com/paper/2402.18677/) (2024)

## Abstract (arXiv)

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 case studies on quadrotor UAV and power converter test systems.