AVERIST Algorithmic Verifier of Stability

The input is defined as an automaton.
Input syntax var: x,v;
location: north, east, south, west;

loc: north;
inv: expression;
dyn: inequality;
guards:
when expression goto 'location name';
when expression goto 'location name';
loc: east;
inv: expression;
dyn: inequality;
guards:
when expression goto 'location name';
when expression goto 'location name';

expr := a*x + b*v {<=,>=,==} k

expr := True

iexpr := a*dx + b*dv {<=,>=,==} k

a,b,k ∈ ℕ


expression := expr AND expr INVARIANT AND GUARD
inequality := iexpr AND iexpr DYNAMICS

You can download some input examples in here.