PRoTECT¶

Parallelized Construction of Safety Barrier Certificates for Nonlinear Polynomial Systems

PRoTECT is an open-source tool for verifying safety properties of dynamical systems through barrier certificate synthesis. It supports four classes of systems — discrete-time and continuous-time, deterministic and stochastic — using sum-of-squares (SOS) optimization with parallelized search across barrier degrees.

Parallelized Search

Searches across multiple barrier polynomial degrees in parallel using multiprocessing for faster certificate discovery.

4 System Types

Supports discrete-time and continuous-time systems, both deterministic and stochastic (dt-DS, dt-SS, ct-DS, ct-SS).

GUI + API

Use the PyQt6 graphical interface for interactive exploration or call functions directly from Python scripts.

SOS Optimization

Employs sum-of-squares optimization programs to systematically search for polynomial-type barrier certificates.

Getting Started¶

Installation

Install PRoTECT and its dependencies on Ubuntu, macOS, or Docker.

Installation

Quick Start

Define a system, compute a barrier certificate, and interpret the results.

Quick Start

Examples

Browse worked examples with figures: jet engine, Van der Pol, two-room, and more.

Examples

API Reference

Complete reference for all barrier computation functions and utilities.

API Reference

Supported System Types¶

System Type	Time	Noise	Functions
Discrete-Time Deterministic (dt-DS)	Discrete	None	`dt_DS`, `parallel_dt_DS`
Discrete-Time Stochastic (dt-SS)	Discrete	Normal, Exponential, Uniform	`dt_SS`, `parallel_dt_SS`
Continuous-Time Deterministic (ct-DS)	Continuous	None	`ct_DS`, `parallel_ct_DS`
Continuous-Time Stochastic (ct-SS)	Continuous	Normal, Exponential, Uniform	`ct_SS`, `parallel_ct_SS`

Citing PRoTECT¶

If you use PRoTECT in your research, please cite:

@inproceedings{wooding2025ictac,
  title={PRoTECT: Parallelized ConstRuction of SafeTy BarriEr
         Certificates for Nonlinear Polynomial SysTems},
  author={Wooding, Ben and Horbanov, Viacheslav and Lavaei, Abolfazl},
  booktitle={International Colloquium on Theoretical Aspects of Computing},
  pages={448--458},
  year={2025},
  organization={Springer}
}