# TIRA: Toolbox for Interval Reachability Analysis

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

## Key facts

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

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

- [GoTube: Scalable Stochastic Verification of Continuous-Depth Models](https://mlsanity.com/paper/2107.08467/) (2021)
- [Learning Density Distribution of Reachable States for Autonomous Systems](https://mlsanity.com/paper/2109.06728/) (2021)
- [Interval Reachability of Nonlinear Dynamical Systems with Neural Network Controllers](https://mlsanity.com/paper/2301.07912/) (2023)
- [Efficient Interaction-Aware Interval Analysis of Neural Network Feedback Loops](https://mlsanity.com/paper/2307.14938/) (2023)
- [A Toolbox for Fast Interval Arithmetic in numpy with an Application to Formal Verification of Neural Network Controlled Systems](https://mlsanity.com/paper/2306.15340/) (2023)
- [Provably Correct Training of Neural Network Controllers Using Reachability Analysis](https://mlsanity.com/paper/2102.10806/) (2021)
- [Mixed Monotonicity Reachability Analysis of Neural ODE: A Trade-Off Between Tightness and Efficiency](https://mlsanity.com/paper/2510.17859/) (2025)
- [Provably Safe Model-Based Meta Reinforcement Learning: An Abstraction-Based Approach](https://mlsanity.com/paper/2109.01255/) (2021)
- [TNODEV: Toolbox for Neural ODE Verification](https://mlsanity.com/paper/2606.16567/) (2026)
- [Certifying Safety in Reinforcement Learning under Adversarial Perturbation Attacks](https://mlsanity.com/paper/2212.14115/) (2022)
- [Convex Hulls of Reachable Sets](https://mlsanity.com/paper/2303.17674/) (2023)
- [Robustness Analysis of Continuous-Depth Models with Lagrangian Techniques](https://mlsanity.com/paper/2308.12192/) (2023)

## Abstract (arXiv)

This paper presents TIRA, a Matlab library gathering several methods for the computation of interval over-approximations of the reachable sets for both continuous- and discrete-time nonlinear systems. Unlike other existing tools, the main strength of interval-based reachability analysis is its simplicity and scalability, rather than the accuracy of the over-approximations. The current implementation of TIRA contains four reachability methods covering wide classes of nonlinear systems, handled with recent results relying on contraction/growth bounds and monotonicity concepts. TIRA's architecture features a central function working as a hub between the user-defined reachability problem and the library of available reachability methods. This design choice offers increased extensibility of the library, where users can define their own method in a separate function and add the function call in the hub function.