Correct-by-Construction Barrier Certificate Synthesis for Safety Verification of Continuous Dynamical Systems

Barrier certificates are a powerful tool for verifying the safety of dynamical systems by certifying that trajectories remain within a safe region while avoiding unsafe states. However, due to the parametric nature of their synthesis procedure and the inaccuracies resulting from the required numerical solvers, constructing valid barrier certificates is challenging, requiring post-synthesis verification to confirm their correctness. This paper presents a combined framework for correct-by-construction barrier certificate synthesis by combining barrier certificate synthesis witnessing dynamical systems safety with polynomial synthesis witnessing the resulting real arithmetic via a combination of semidefinite programming (SDP) and Gröbner bases for the Real Nullstellensatz. This is achieved by exploiting a sum-of-squares relaxation for both the barrier certificate and Real Nullstellensatz witness construction procedures by solving a single combined sum-of-squares optimization program, hence eliminating the need for post-synthesis verification. We also show how a monomial basis for the witness can be chosen. We demonstrate the effectiveness of our framework on some examples, showcasing its ability to certify safety by synthesizing correct-by-construction barrier certificates.