  We present a method for computing exact reachable sets for deep neural
networks with rectified linear unit (ReLU) activation. Our method is
well-suited for use in rigorous safety analysis of robotic perception and
control systems with deep neural network components. Our algorithm can compute
both forward and backward reachable sets for a ReLU network iterated over
multiple time steps, as would be found in a perception-action loop in a robotic
system. Our algorithm is unique in that it builds the reachable sets by
incrementally enumerating polyhedral cells in the input space, rather than
iterating layer-by-layer through the network as in other methods. If an unsafe
cell is found, our algorithm can return this result without completing the full
reachability computation, thus giving an anytime property that accelerates
safety verification. In addition, our method requires less memory during
execution compared to existing methods where memory can be a limiting factor.
We demonstrate our algorithm on safety verification of the ACAS Xu aircraft
advisory system. We find unsafe actions many times faster than the fastest
existing method and certify no unsafe actions exist in about twice the time of
the existing method. We also compute forward and backward reachable sets for a
learned model of pendulum dynamics over a 50 time step horizon in 87s on a
laptop computer. Algorithm source code:
https://github.com/StanfordMSL/Neural-Network-Reach.
