Barrifier

Stefan Ratschan

Barrifier is a program for verifying safety of dynamical systems. It proves safety using barrier certificates and computes counter-example trajectories using numerical optimization. The current version still is very much of a prototype but we will continuously improve the software in the near future.

Download (64bit Linux)

Support:

The quality of this package depends heavily on your feedback. So if you found a bug, have an example where Barrifier works particularily bad/well, or if you have any other questions, please send an e-mail to email

Documentation:

HTML
PDF

Main Paper Describing Method

Stefan Ratschan
Simulation Based Computation of Certificates for Safety of Dynamical Systems
Proc. FORMATS 2017, Springer LNCS 10419
DOI ArXiv BIB

Software Dependencies:

The package use the SMT solver OptiMathSAT which you will need to download separately, and the packages NLOPT and SUNDIALS which are built in.

Copying:

This software is available under the GNU Lesser General Public License. We ask you to properly cite its use in resulting applications and publications.

I would appreciate it, if you notify me ( email ) of your use of Barrifier, inform me about bugs, and send me resulting publications.

Acknowledgements:

This software package was supported by GAČR grant 15-14484S and by the long-term strategic development financing of the Institute of Computer Science (RVO:67985807).