# Safe Reach Set Computation via Neural Barrier Certificates

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

## Key facts

- Cited by 5 papers in the map (data through 14 Oct 2026).
- Builds on 13 of its 34 references that are in the map.
- First posted on arXiv 29 Apr 2024.

## Builds on (most cited first, 13 of 13)

- [Control Barrier Function Based Quadratic Programs for Safety Critical Systems](https://mlsanity.com/paper/1609.06408/) (2016)
- [Learning Model Predictive Control for iterative tasks. A Data-Driven Control Framework](https://mlsanity.com/paper/1609.01387/) (2016)
- [Synthesis of Control Barrier Functions Using a Supervised Machine Learning Approach](https://mlsanity.com/paper/2003.04950/) (2020)
- [Neural Certificates for Safe Control Policies](https://mlsanity.com/paper/2006.08465/) (2020)
- [JuliaReach: a Toolbox for Set-Based Reachability](https://mlsanity.com/paper/1901.10736/) (2019)
- [Learning Safe Neural Network Controllers with Barrier Certificates](https://mlsanity.com/paper/2009.09826/) (2020)
- [Case Study: Verifying the Safety of an Autonomous Racing Car with a Neural Network Controller](https://mlsanity.com/paper/1910.11309/) (2019)
- [Towards a Framework for Certification of Reliable Autonomous Systems](https://mlsanity.com/paper/2001.09124/) (2020)
- [Data-Driven Distributionally Robust Safety Verification Using Barrier Certificates and Conditional Mean Embeddings](https://mlsanity.com/paper/2403.10497/) (2024)
- [Formal Policy Synthesis for Continuous-Space Systems via Reinforcement Learning](https://mlsanity.com/paper/2005.01319/) (2020)
- [Automated and Formal Synthesis of Neural Barrier Certificates for Dynamical Models](https://mlsanity.com/paper/2007.03251/) (2020)
- [Synthesizing Invariant Barrier Certificates via Difference-of-Convex Programming](https://mlsanity.com/paper/2105.14311/) (2021)
- [Formal verification of octorotor flight envelope using barrier functions and SMT solving](https://mlsanity.com/paper/2107.00612/) (2021)

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

- [Formally Verifying Deep Reinforcement Learning Controllers with Lyapunov Barrier Certificates](https://mlsanity.com/paper/2405.14058/) (2024)
- [Bridging Control with Neural Network Verifier alpha-beta-CROWN: A Tutorial](https://mlsanity.com/paper/2605.26577/) (2026)
- [BarrierBench: Evaluating Large Language Models for Safety Verification in Dynamical Systems](https://mlsanity.com/paper/2511.09363/) (2025)
- [Neural Proofs for Sound Verification and Control of Complex Systems](https://mlsanity.com/paper/2512.18389/) (2025)
- [Kernel-Based Learning of Safety Barriers](https://mlsanity.com/paper/2601.12002/) (2026)

## Abstract (arXiv)

We present a novel technique for online safety verification of autonomous systems, which performs reachability analysis efficiently for both bounded and unbounded horizons by employing neural barrier certificates. Our approach uses barrier certificates given by parameterized neural networks that depend on a given initial set, unsafe sets, and time horizon. Such networks are trained efficiently offline using system simulations sampled from regions of the state space. We then employ a meta-neural network to generalize the barrier certificates to state space regions that are outside the training set. These certificates are generated and validated online as sound over-approximations of the reachable states, thus either ensuring system safety or activating appropriate alternative actions in unsafe scenarios. We demonstrate our technique on case studies from linear models to nonlinear control-dependent models for online autonomous driving scenarios.