This is the homepage of the toolbox version of Flow*. The first version of Flow* was released in the year of 2013, and improved in 2015 (version 1.2.0) and 2017 (version 2.1.0). The purpose of releasing a toolbox version is to provide a more flexible way to model and analyze cyber-physical systems (CPS), and expose the key functions to the tools for verifying more complex systems, such as the CPS with machine learning components. The main data structures in the toolbox version are completely re-designed and implemented such that the performance is at least 10x faster than the version 2.1.0 on hybrid case studies.
Flow* is mainly used to compute reachable set overapproximations which are guranteed to contain all approximation and numerical errors. The following video shows an example of using Flow* on a mobile device to online detect the future unsafety for the RC car.
Flow* is also used to verify dynamical systems controlled by neural networks. Please check our tool POLAR.
The Flow* toolbox does not have a specific interface, it is compiled as a static library. A verification or reachability task should be described as a C++ file which can be compiled with the Flow* libarary.
Time-bounded reachability computation. Flow computes Taylor Model (TM) flowpipes for a discrete, continuous or hybrid dynamics over a bounded time interval. TMs are function* rather than pure range overapproximations. As it is illustrated by the following figure, a TM overapproximates the flowmap of a deterministic dynamics, and its range forms an overapproximation of the reachable set.
Safety verification. Conservatively checking the intersection of the TM flowpipe ranges with a given safe or unsafe set.
Configuration independent relational abstraction for linear dynamics. The Flow* toolbox does not directly compute reachable set overapproximations for Linear Time-Invariant (LTI) or Linear Time-Varying (LTV) ODEs. Instead, it generates TM overapproximations for the flowmap functions that maps any initial state to its reachable state at a time. Such abstractions may be reused in verification tasks for different system settings.
The tool can also be used to find potential counterexamples when the overapproximated flowmap is deterministic. E.g., when an unsafe intersection is detected for a TM $p(x_0,t)$, you may use the domain contraction function to reduce $x_0$'s range, which is the initial set, and find an overapproximation of the unsafe initial states.
The following GNU open-source libraries should be pre-installed: M4, GMP, MPFR, GSL, GLPK, BISON, FLEX. Most of them are available at https://ftp.gnu.org/.
Flow* does not require an installation. You may simply run make to compile the source code and a static library file libflowstar.a will be generated. The compilation should be done by GCC 8.0 or a later version. You may need to rename 'g++' in the makefile to ensure that an appropriate compiler is called.
We present a very simple nonlinear ODE which only has a single state variable:
$$\dot{x} = 1 - \sin(x) \ \frac{\sqrt{\log(x)}}{\exp(\cos(x))}$$
We want to compute its reachable set from the initial state set $x(0)\in {[4.8,5.2]}$.
The above reachability problem can be described by the following C++ program using the Flow* library.
![]() |
![]() |
![]() |
Cutoff threshold: 1e-5 Time cost: 4.6 seconds |
Cutoff threshold: 1e-6 Time cost: 5.6 seconds |
Cutoff threshold: 1e-7 Time cost: 7.3 seconds |
Laub-Loomis Model (radius 0.1)
![]() |
![]() |
Symbolic remainder size: 0 Time cost: 5.3 seconds (M1 Mac mini) |
Symbolic remainder size: 20 Time cost: 3.9 seconds (M1 Mac mini) |
-- More content will be added.
[1] Xin Chen, Erika Abraham, Sriram Sankaranarayanan. Taylor Model Flowpipe Construction for Non-linear Hybrid Systems. In Real Time Systems Symposium (RTSS), pp. 183-192, 2012. (link)
[2] Xin Chen, Erika Abraham, Sriram Sankaranarayanan. Flow: An Analyzer for Non-Linear Hybrid Systems.* In Computer-Aided Verification (CAV), volume 8044 of LNCS, pp. 258-263, 2013. (link)
[3] Xin Chen. Reachability Analysis of Non-Linear Hybrid Systems Using Taylor Models. Ph.D. Thesis, RWTH Aachen University, 2015. (link)
[4] Xin Chen, Sriram Sankaranarayanan. Decomposed Reachability Analysis for Nonlinear Systems. In Real-Time Systems Symposium (RTSS), 2016. (link)
[5] Xin Chen, Sergio Mover, and Sriram Sankaranarayanan. Compositional Relational Abstraction for Nonlinear Hybrid Systems. In ACM Transactions on Embedded Computing Systems (TECS) 16(5): pp. 187:1-187:19, 2017. (link)