# JuliaReach: a Toolbox for Set-Based Reachability

arXiv: https://arxiv.org/abs/1901.10736 · HTML: https://mlsanity.com/paper/1901.10736/

## Key facts

- Cited by 28 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 30 Jan 2019.

## Built on by (most cited first, 28 of 28)

- [Verification of Neural-Network Control Systems by Integrating Taylor Models and Zonotopes](https://mlsanity.com/paper/2112.09197/) (2021)
- [Open- and Closed-Loop Neural Network Verification using Polynomial Zonotopes](https://mlsanity.com/paper/2207.02715/) (2022)
- [Vehicle: Bridging the Embedding Gap in the Verification of Neuro-Symbolic Programs](https://mlsanity.com/paper/2401.06379/) (2024)
- [Reachability Analysis of a General Class of Neural Ordinary Differential Equations](https://mlsanity.com/paper/2207.06531/) (2022)
- [Neural Network Verification is a Programming Language Challenge](https://mlsanity.com/paper/2501.05867/) (2025)
- [Neural Abstractions](https://mlsanity.com/paper/2301.11683/) (2023)
- [Efficient Interaction-Aware Interval Analysis of Neural Network Feedback Loops](https://mlsanity.com/paper/2307.14938/) (2023)
- [Shielded Reinforcement Learning for Hybrid Systems](https://mlsanity.com/paper/2308.14424/) (2023)
- [Formal Verification of Graph Convolutional Networks with Uncertain Node Features and Uncertain Graph Structure](https://mlsanity.com/paper/2404.15065/) (2024)
- [Scalable Surrogate Verification of Image-based Neural Network Control Systems using Composition and Unrolling](https://mlsanity.com/paper/2405.18554/) (2024)
- [Neural Predictive Monitoring under Partial Observability](https://mlsanity.com/paper/2108.07134/) (2021)
- [Provably Safe Neural Network Controllers via Differential Dynamic Logic](https://mlsanity.com/paper/2402.10998/) (2024)
- [Fully Automatic Neural Network Reduction for Formal Verification](https://mlsanity.com/paper/2305.01932/) (2023)
- [Safe Reach Set Computation via Neural Barrier Certificates](https://mlsanity.com/paper/2404.18813/) (2024)
- [textttimmrax: A Parallelizable and Differentiable Toolbox for Interval Analysis and Mixed Monotone Reachability in JAX](https://mlsanity.com/paper/2401.11608/) (2024)
- [Robustness Verification of Deep Neural Networks using Star-Based Reachability Analysis with Variable-Length Time Series Input](https://mlsanity.com/paper/2307.13907/) (2023)
- [Learning-Based Approaches to Predictive Monitoring with Conformal Statistical Guarantees](https://mlsanity.com/paper/2312.01959/) (2023)
- [Parallel Differentiable Reachability for Learning and Planning with Certified Neural Dynamics and Controllers](https://mlsanity.com/paper/2605.25346/) (2026)
- [Learning Provably Robust Motion Planners Using Funnel Libraries](https://mlsanity.com/paper/2111.08733/) (2021)
- [Abstract Interpretation for Generalized Heuristic Search in Model-Based Planning](https://mlsanity.com/paper/2208.02938/) (2022)
- [The inverse problem for neural networks](https://mlsanity.com/paper/2308.14093/) (2023)
- [Formal Verification of Long Short-Term Memory based Audio Classifiers: A Star based Approach](https://mlsanity.com/paper/2311.12130/) (2023)
- [Compositional Inductive Invariant Based Verification of Neural Network Controlled Systems](https://mlsanity.com/paper/2312.10842/) (2023)
- [The Reachability Problem for Neural-Network Control Systems](https://mlsanity.com/paper/2407.04988/) (2024)
- [Training Verifiably Robust Agents Using Set-Based Reinforcement Learning](https://mlsanity.com/paper/2408.09112/) (2024)
- [Of Good Demons and Bad Angels: Guaranteeing Safe Control under Finite Precision](https://mlsanity.com/paper/2507.22760/) (2025)
- [Architectural Transformations and Emerging Verification Demands in AI-Enabled Cyber-Physical Systems](https://mlsanity.com/paper/2510.00519/) (2025)
- [NNV3: Expanding Neural Network Verification to New Architectures and Domains](https://mlsanity.com/paper/2609.30050/) (2026)

## Abstract (arXiv)

We present JuliaReach, 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.