Visible to the public SAPOConflict Detection Enabled

Submitted by akarns on Mon, 11/20/2017 - 3:05pm

Sapo

Description: Sapo is a C++ tool for the formal analysis of discrete-time polynomial dynamical systems.

The problems treated by Sapo are:

  • Reachability computation, i.e., the calculation of the set of states reachable by the system from a set of initial conditions
  • Parameter synthesis, i.e., the refinement of a set of parameters so that the system satisfies a given specification.

For reachability analysis Sapo produces a flowpipe that over-approximates the set of states reachable by the system from a set of initial conditions.

For parameter synthesis Sapo computes a refinement of the given set of parameters such that the system satisfies a given specification. The specification is formalized as a Signal Temporal Logic (STL) formula.

In both cases, the analysis can be done on bounded time.

VO Integration: No

Active: No

Available Benchmarks: No

Website: None

Download: Github repo

Documentation: Links to a tool paper and slides. See also the readme of the repository linked above.

Contact: Tommaso Dreossi

Backlinks: