Overview: Beaver tool has implemented in python 2.7 and it provides a framework for safety verification of parameterized linear dynamical system. It uses z3-SMT solver version 4.3.2. The tool takes the input system matrices, initial set as a compact polyhedral set, time horizon T, error tolerance ε > 0, and unsafe region. The tool gives an output in the form of the SMT expression, which is in SMT Lib format.
Instruction to run: Beaver tool has 3 folder:
- main
- source
- library
Installation: There are following software, which are required to install before running beaver tool:
- Python 2.7
- z3
Syntax: