** Beaver: ** This is a tool for computing the
over-approximate reach set of the parameterized linear dynamical system given by,

**ẋ**(t) = A

**x**(t),

**x**(0) ∈

**X**

_{0}⊆

^{n}, A ∈

**Ω**, t ∈ [0,T] (1)

**X**

_{0}and

**Ω**⊆

^{n×n}, are compact polyhedral sets, A is a n×n dimensional matrix and [0,T] is the time domain of interest. This tool computes the over approximate reach set in the form of SMT expressions in SMT Lib format. We use Z3-SMT solver for safety verification of system (1) from the given unsafe region.

**Reach set: **
The state of the System (1) starting from an initial state **x**(0) ∈ **X**_{0}
for a matrix A ∈ **Ω** at time t is given by the state transition function defined as:

**x**(0), A, t) = e

^{At}

**x**(0)

_{Φ}(

**X**(0), Ω, [0,T]) = {Φ(

**x**(0), A, t) |

**x**(0) ∈

**X**

_{0}, A ∈

**Ω**, t ∈ [0,T]}

**Verification: ** This tool is useful for safety verification
of the reach set of the parameterized linear dynamical system from the given unsafe region. It is shown in
below figure.

_{Φ }(

**X**(0), Ω, [0,T]) does not intersect with unsafe region, i.e. it is safe and if the output is sat, the ε-ball of reach set B

_{ε}(Reach

_{Φ}(

**X**(0), Ω, [0,T])) intersects with the unsafe region i.e. it is Unsafe

^{*}. The Unsafe

^{*}guarantees that the reach set of the parameterized linear dynamical system is unsafe within the error tolerance ε > 0.