A collection of reachability calculation toolboxes and software
| Name | Language | Feature |
|---|---|---|
| Level-set Toolbox | MATLAB | Solves Hamilton-Jacobi-Issacs equation for reachability analysis using level-set approximation |
| BEACLS | C++ | A C++ implementation of the level-set methods for reachability analysis |
| FaSTrack | C++ | Fast planning methods with slower, reachability-based safety guarantees for online trajectory planning in ROS framework |
| KeYmaera X | Java | A theorem prover for differential dynamic logic |
| MPT | MATLAB | Provides reachable set and invariance set calculation for linear, nonlinear and hybrid systems |
| dReach | C++ | A bounded reachability analysis tool for hybrid systems |
| SpaceEx | C++ | A platform for the implementation of algorithms related to reachability and safety verification |
| CommonRoad | Python | A collection of composable benchmarks for motion planning on roads, which provides researchers with a means of evaluating and comparing their motion planners |
| CommonRoad-Reach | Python/C++ | A Python interfaced forward reachable set and 'drivable corridor' computation tool integrated with the CommonRoad eco-system |
| SPOT | MATLAB | A tool to predict the future occupancy of other traffic participants using reachable sets |
| CORA | MATLAB | A collection of MATLAB classes for the formal verification of cyber-physical systems using reachability analysis |
| Flow* | C++ | An efficient tool to calculate reachability for polynomial-based hybrid systems |
| ARIANDE | C++/Python | C++/Python library for formal verification of cyber-physical systems, using reachability analysis and rigorous numerics on nonlinear hybrid automata |
| HyCreate | Java | A tool for overapproximating reachability of hybrid automata using union of boxes to overapproximate reachable sets |
| Hylaa | Python | A verification tool for system models with linear ODEs, time-varying inputs, and possibly hybrid dynamics |
| NNV | MATLAB | Implements reachability methods for analyzing neural networks, particularly with a focus on closed-loop controllers in autonomous cyber-physical systems (CPS) |
| JuliaReach | Julia | Reachability computations for dynamical systems in Julia |
| C2E2 | Python | C2E2 can automatically check bounded time invariant properties of nonlinear hybrid automata |
| DryVR | Python | Framework for probabilistic algorithm for learning sensitivity from simulation data, and bounded reachability analysis that uses the learned sensitivity |
| AROC | MATLAB | A toolbox to automatically synthesizes verified controllers for solving reach-avoid problems using reachability analysis |
| CoSyMa(pdf) | ML | A tool for controller synthesis using multi-scale abstractions |
| NeuReach(pdf) | Python | A tool that uses neural networks for predicting reachable sets from executions of a dynamical system |
| Co4Pro(pdf) | MATLAB | Correct by Construction Controllers from Control Programs (Toolbox) |
(table generated using Tables Generator)
To cite this table, use the citation of the full paper: Formal Certification Methods for Automated Vehicle Safety Assessment
Feel free to suggest other tools to be added in the list, by creating an Issue in Issues or by pull request.