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).