Ben Wooding

PRoTECT Software Tool

PRoTECT: Parallelized Construction of Safety Barrier Certificates for Nonlinear Polynomial Systems

PRoTECT jet-engine case study: barrier-certificate level sets separating trajectories starting in the initial set from the unsafe region

PRoTECT is an open-source software tool for the parallelized construction of safety barrier certificates (BCs) for nonlinear polynomial systems. This tool employs sum-of-squares (SOS) optimization programs to systematically search for polynomial-type BCs. It can verify safety properties over four classes of dynamical systems: (i) discrete-time stochastic systems, (ii) discrete-time deterministic systems, (iii) continuous-time stochastic systems, and (iv) continuous-time deterministic systems.

PRoTECT is implemented in Python as an application programming interface (API). It includes a user-friendly graphic user interface (GUI) or interaction via function calls from other Python programs. PRoTECT leverages parallelism across different barrier degrees to efficiently search for a feasible BC. The GitHub repository for PRoTECT can be found at Kiguli/PRoTECT. You can also find some useful videos for installing and understanding PRoTECT below.

ICTAC paper Extended arXiv paper ICCPS Poster Abstract View on GitHub

Used in

Independent groups that have run PRoTECT as a baseline in their own evaluations.

Competitions

Entered in the ARCH-COMP friendly verification competition and run on the community benchmark suite. Category reports are co-authored by the participating teams.