JuliaReach is a toolbox for set-based reachability analysis of dynamical systems. JuliaReach consists of two main packages: Reachability, containing implementations of reachability algorithms for continuous and hybrid systems, and LazySets, a standalone library that implements state-of-the-art algorithms for calculus with convex sets. The library offers both concrete and lazy set representations, where the latter stands for the ability to delay set computations until they are needed. The choice of the programming language Julia and the accompanying documentation of our toolbox allow researchers to easily translate set-based algorithms from mathematics to software in a platform-independent way, while achieving runtime performance that is comparable to statically compiled languages. Combining lazy operations in high dimensions and explicit computations in low dimensions, JuliaReach can be applied to solve complex, large-scale problems.
- LazySets.jl A Julia package for calculus with convex sets.
- Reachability.jl Reachability and Safety of Nondeterministic Dynamical Systems.
- SX.jl SpaceEx modeling language parser.
- MathematicalSystems.jl Systems definitions in Julia.
- BernsteinExpansions.jl A Julia package to compute Bernstein coefficients of multivariate polynomials.
Two-dimensional switched oscillator and a parametric number of filters (here 256)
Hybrid model of a cruise control with service and emergency brakes of the engine
Transition into aborting mode of the linear hybrid spacecraft rendez-vous model
Nonlinear dynamics of a quadrotor: verifying stabilization with a PD controller
Nononlinear Laub-Loomis model studying a class of enzymatic activities
using Reachability # Laub-Loomis is a seven-dimensional ODE with quadratic nonlinearities
Structural model of component 1R (Russian service module) with 270 state variables
Verification that the top-floor displacement of a building is below a given bound
Benchmarks & Repeatability Evaluations
- ARCH18. 5th International Workshop on Applied Verification of Continuous and Hybrid Systems.
- HSCC19. 22nd ACM International Conference on Hybrid Systems: Computation and Control.
- ARCH19. 6th International Workshop on Applied Verification of Continuous and Hybrid Systems.
- Marcelo Forets. Universidad de la República, Uruguay.
- Kostiantyn Potomkin. Australian National University, Australia.
- Christian Schilling. Institute for Science and Technology, Austria.
- Luis Benet. Instituto de Ciencias Físicas, Universidad Nacional Autónoma de México, México.
- Sergiy Bogomolov. College of Engineering & Computer Science, Australian National University, Australia.
- Goran Frehse. ENSTA ParisTech, France.
- Andreas Podelski. University of Freiburg, Germany.
- David P. Sanders. Departamento de Física, Facultad de Ciencias, Universidad Nacional Autónoma de México, México.
- Frédéric Viry. CERFACS, France.