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:

  1. main
  2. source
  3. library
The main folder has the main program named as main.py, the initial set file named as initial_set.txt, the system matrices file named as system_matrix.txt, the output file named as sat.smt, and the unsafe region file named as unsafe_region.txt. The source folder has all the implementation files. The library folder contains the library packages, which are used in beaver tool.

Installation: There are following software, which are required to install before running beaver tool:

  • Python 2.7
  • z3

Syntax:

Input Syntax: var: ε, T;
Initial_set: X0;
System_matrix: Ω
Unsafe_region: R

Output Format: SMT_expression;