Reachability is a software for reachability analysis and safety property checking that performs flowpipe computation of dynamical systems given by ordinary differential equations models (ODEs) in continuous or discrete time.
It is written in Julia, a modern high-performance language
for scientific computing.
Currently this package implements algorithms for flowpipe approximation of:
This package requires Julia v1.0 or later. Refer to the official documentation on how to install and run Julia in your system.
The set computations depend on the core library
LazySets.jl, which is also part of the JuliaReach framework.
LazySets.jl exploits the principle of lazy (on-demand) evaluation and uses support functions to represent lazy sets.
The latest stable release of
LazySets.jl is installed automatically when you install
Reachability.jl (see the installation instructions below). See the installation section of
LazySets.jl for further details.
Depending on your needs, choose an appropriate command from the following list
and enter it in Julia's REPL. To activate the
pkg mode, type
] (and to leave it, type
pkg> add https://github.com/JuliaReach/Reachability.jl
pkg> add https://github.com/JuliaReach/Reachability.jl#master
pkg> dev https://github.com/JuliaReach/Reachability.jl