  We present a tool for computing exact forward and backward reachable sets of
deep neural networks with rectified linear unit (ReLU) activation. We then
develop algorithms using this tool to compute invariant sets and regions of
attraction (ROAs) for control systems with neural networks in the feedback
loop. Our algorithm is unique in that it builds the reachable sets by
incrementally enumerating polyhedral regions in the input space, rather than
iterating layer-by-layer through the network as in other methods. When
performing safety verification, if an unsafe region is found, our algorithm can
return this result without completing the full reachability computation, thus
giving an anytime property that accelerates safety verification. Furthermore,
we introduce a method to accelerate the computation of ROAs in the case that
deep learned components are homeomorphisms, which we find is surprisingly
common in practice. We demonstrate our tool in several test cases. We compute a
ROA for a learned van der Pol oscillator model. We find a control invariant set
for a learned torque-controlled pendulum model. We also verify specific safety
properties for multiple deep networks related to the ACAS Xu aircraft collision
advisory system. Finally, we apply our algorithm to find ROAs for an
image-based aircraft runway taxi problem. Algorithm source code:
https://github.com/StanfordMSL/Neural-Network-Reach .
