{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,23]],"date-time":"2026-10-23T20:29:49Z","timestamp":1792787389304,"version":"4.5.0"},"reference-count":40,"publisher":"Association for Computing Machinery (ACM)","issue":"5s","license":[{"start":{"date-parts":[[2019,10,8]],"date-time":"2019-10-08T00:00:00Z","timestamp":1570492800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1834701, 1834324, 1839511, 1724341"],"award-info":[{"award-number":["1834701, 1834324, 1839511, 1724341"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"name":"NSF grant","award":["CCF-1646497"],"award-info":[{"award-number":["CCF-1646497"]}]},{"name":"DARPA BRASS program","award":["FA8750-16-C-0043"],"award-info":[{"award-number":["FA8750-16-C-0043"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Embed. Comput. Syst."],"published-print":{"date-parts":[[2019,10,31]]},"abstract":"<jats:p>Applying neural networks as controllers in dynamical systems has shown great promises. However, it is critical yet challenging to verify the safety of such control systems with neural-network controllers in the loop. Previous methods for verifying neural network controlled systems are limited to a few specific activation functions. In this work, we propose a new reachability analysis approach based on Bernstein polynomials that can verify neural-network controlled systems with a more general form of activation functions, i.e., as long as they ensure that the neural networks are Lipschitz continuous. Specifically, we consider abstracting feedforward neural networks with Bernstein polynomials for a small subset of inputs. To quantify the error introduced by abstraction, we provide both theoretical error bound estimation based on the theory of Bernstein polynomials and more practical sampling based error bound estimation, following a tight Lipschitz constant estimation approach based on forward reachability analysis. Compared with previous methods, our approach addresses a much broader set of neural networks, including heterogeneous neural networks that contain multiple types of activation functions. Experiment results on a variety of benchmarks show the effectiveness of our approach.<\/jats:p>","DOI":"10.1145\/3358228","type":"journal-article","created":{"date-parts":[[2019,10,10]],"date-time":"2019-10-10T09:13:05Z","timestamp":1570698785000},"page":"1-22","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":144,"title":["ReachNN"],"prefix":"10.1145","volume":"18","author":[{"given":"Chao","family":"Huang","sequence":"first","affiliation":[{"name":"Northwestern University, Evanston, Illinois"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jiameng","family":"Fan","sequence":"additional","affiliation":[{"name":"Boston University, Boston, Massachusetts"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Wenchao","family":"Li","sequence":"additional","affiliation":[{"name":"Boston University, Boston, Massachusetts"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Xin","family":"Chen","sequence":"additional","affiliation":[{"name":"University of Dayton, Dayton, Ohio"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Qi","family":"Zhu","sequence":"additional","affiliation":[{"name":"Northwestern University, Evanston, Illinois"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,10,8]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Proc. of ARCH\u201915 (EPiC Series in Computer Science)","volume":"34","author":"Althoff M.","year":"2015","unstructured":"M. Althoff . 2015 . An introduction to CORA 2015 . In Proc. of ARCH\u201915 (EPiC Series in Computer Science) , Vol. 34 . EasyChair, 120--151. M. Althoff. 2015. An introduction to CORA 2015. In Proc. of ARCH\u201915 (EPiC Series in Computer Science), Vol. 34. EasyChair, 120--151."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00202-T"},{"key":"e_1_2_1_3_1","unstructured":"Jimmy Ba and Rich Caruana. 2014. Do deep nets really need to be deep?. In Advances in Neural Information Processing Systems. 2654--2662.  Jimmy Ba and Rich Caruana. 2014. Do deep nets really need to be deep?. In Advances in Neural Information Processing Systems. 2654--2662."},{"key":"e_1_2_1_4_1","volume-title":"Sterling","author":"Beer Randall D.","year":"1989","unstructured":"Randall D. Beer , Hillel J. Chiel , and Leon S . Sterling . 1989 . Heterogeneous neural networks for adaptive behavior in dynamic environments. In Advances in Neural Information Processing Systems . 577--585. Randall D. Beer, Hillel J. Chiel, and Leon S. Sterling. 1989. Heterogeneous neural networks for adaptive behavior in dynamic environments. In Advances in Neural Information Processing Systems. 577--585."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1024467732637"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/0021-9045(87)90087-6"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1150402.1150464"},{"key":"e_1_2_1_9_1","volume-title":"Proc. of RTSS\u201912","author":"Chen X.","unstructured":"X. Chen , E. \u00c1brah\u00e1m , and S. Sankaranarayanan . 2012. Taylor model flowpipe construction for non-linear hybrid systems . In Proc. of RTSS\u201912 . IEEE Computer Society, 183--192. X. Chen, E. \u00c1brah\u00e1m, and S. Sankaranarayanan. 2012. Taylor model flowpipe construction for non-linear hybrid systems. In Proc. of RTSS\u201912. IEEE Computer Society, 183--192."},{"key":"e_1_2_1_10_1","volume-title":"Proc. of CAV\u201913 (LNCS)","volume":"8044","author":"Chen X.","unstructured":"X. Chen , E. \u00c1brah\u00e1m , and S. Sankaranarayanan . 2013. Flow*: An analyzer for non-linear hybrid systems . In Proc. of CAV\u201913 (LNCS) , Vol. 8044 . Springer, 258--263. X. Chen, E. \u00c1brah\u00e1m, and S. Sankaranarayanan. 2013. Flow*: An analyzer for non-linear hybrid systems. In Proc. of CAV\u201913 (LNCS), Vol. 8044. Springer, 258--263."},{"key":"e_1_2_1_11_1","volume-title":"2016 IEEE Real-Time Systems Symposium (RTSS). IEEE Press, 13--24","author":"Chen X.","unstructured":"X. Chen and S. Sankaranarayanan . 2016. Decomposed reachability analysis for nonlinear systems . In 2016 IEEE Real-Time Systems Symposium (RTSS). IEEE Press, 13--24 . X. Chen and S. Sankaranarayanan. 2016. Decomposed reachability analysis for nonlinear systems. In 2016 IEEE Real-Time Systems Symposium (RTSS). IEEE Press, 13--24."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9939-1959-0113131-7"},{"key":"e_1_2_1_13_1","doi-asserted-by":"crossref","unstructured":"T. Dreossi T. Dang and C. Piazza. 2016. Parallelotope bundles for polynomial reachability. In HSCC. ACM 297--306.  T. Dreossi T. Dang and C. Piazza. 2016. Parallelotope bundles for polynomial reachability. In HSCC. ACM 297--306.","DOI":"10.1145\/2883817.2883838"},{"key":"e_1_2_1_14_1","volume-title":"Proc. of TACAS\u201915 (LNCS)","volume":"9035","author":"Duggirala P. S.","unstructured":"P. S. Duggirala , S. Mitra , M. Viswanathan , and M. Potok . 2015. C2E2: A verification tool for stateflow models . In Proc. of TACAS\u201915 (LNCS) , Vol. 9035 . Springer, 68--82. P. S. Duggirala, S. Mitra, M. Viswanathan, and M. Potok. 2015. C2E2: A verification tool for stateflow models. In Proc. of TACAS\u201915 (LNCS), Vol. 9035. Springer, 68--82."},{"key":"e_1_2_1_15_1","doi-asserted-by":"crossref","unstructured":"S. Dutta X. Chen and S. Sankaranarayanan. 2019. Reachability analysis for neural feedback systems using regressive polynomial rule inference. In Hybrid Systems: Computation and Control (HSCC). ACM Press 157--168.  S. Dutta X. Chen and S. Sankaranarayanan. 2019. Reachability analysis for neural feedback systems using regressive polynomial rule inference. In Hybrid Systems: Computation and Control (HSCC). ACM Press 157--168.","DOI":"10.1145\/3302504.3311807"},{"key":"e_1_2_1_16_1","volume-title":"NASA Formal Methods Symposium. Springer, 121--138","author":"Dutta S.","unstructured":"S. Dutta , S. Jha , S. Sankaranarayanan , and A. Tiwari . 2018. Output range analysis for deep feedforward neural networks . In NASA Formal Methods Symposium. Springer, 121--138 . S. Dutta, S. Jha, S. Sankaranarayanan, and A. Tiwari. 2018. Output range analysis for deep feedforward neural networks. In NASA Formal Methods Symposium. Springer, 121--138."},{"key":"e_1_2_1_17_1","volume-title":"PHAVer: Algorithmic verification of hybrid systems past HyTech","author":"Frehse G.","unstructured":"G. Frehse . 2005. PHAVer: Algorithmic verification of hybrid systems past HyTech . In HSCC. Springer , 258--273. G. Frehse. 2005. PHAVer: Algorithmic verification of hybrid systems past HyTech. In HSCC. Springer, 258--273."},{"key":"e_1_2_1_18_1","volume-title":"Proc. of CAV\u201911 (LNCS)","volume":"6806","author":"Frehse G.","unstructured":"G. Frehse , C. Le Guernic , A. Donz\u00e9 , S. Cotton , R. Ray , O. Lebeltel , R. Ripado , A. Girard , T. Dang , and O. Maler . 2011. SpaceEx: Scalable verification of hybrid systems . In Proc. of CAV\u201911 (LNCS) , Vol. 6806 . Springer, 379--395. G. Frehse, C. Le Guernic, A. Donz\u00e9, S. Cotton, R. Ray, O. Lebeltel, R. Ripado, A. Girard, T. Dang, and O. Maler. 2011. SpaceEx: Scalable verification of hybrid systems. In Proc. of CAV\u201911 (LNCS), Vol. 6806. Springer, 379--395."},{"key":"e_1_2_1_19_1","unstructured":"Eduardo Gallestey and Peter Hokayem. 2019. Lecture notes in Nonlinear Systems and Control.  Eduardo Gallestey and Peter Hokayem. 2019. Lecture notes in Nonlinear Systems and Control."},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1006\/jcss.1998.1581"},{"key":"e_1_2_1_21_1","volume-title":"Distilling the knowledge in a neural network. CoRR abs\/1503.02531","author":"Hinton Geoffrey E.","year":"2015","unstructured":"Geoffrey E. Hinton , Oriol Vinyals , and Jeffrey Dean . 2015. Distilling the knowledge in a neural network. CoRR abs\/1503.02531 ( 2015 ). Geoffrey E. Hinton, Oriol Vinyals, and Jeffrey Dean. 2015. Distilling the knowledge in a neural network. CoRR abs\/1503.02531 (2015)."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3126508"},{"key":"e_1_2_1_23_1","volume-title":"International Conference on Computer Aided Verification. Springer, 3--29","author":"Huang X.","unstructured":"X. Huang , M. Kwiatkowska , S. Wang , and M. Wu . 2017. Safety verification of deep neural networks . In International Conference on Computer Aided Verification. Springer, 3--29 . X. Huang, M. Kwiatkowska, S. Wang, and M. Wu. 2017. Safety verification of deep neural networks. In International Conference on Computer Aided Verification. Springer, 3--29."},{"key":"e_1_2_1_24_1","volume-title":"Verisig: Verifying safety properties of hybrid systems with neural network controllers. arXiv preprint arXiv:1811.01828","author":"Ivanov Radoslav","year":"2018","unstructured":"Radoslav Ivanov , James Weimer , Rajeev Alur , George J. Pappas , and Insup Lee . 2018 . Verisig: Verifying safety properties of hybrid systems with neural network controllers. arXiv preprint arXiv:1811.01828 (2018). Radoslav Ivanov, James Weimer, Rajeev Alur, George J. Pappas, and Insup Lee. 2018. Verisig: Verifying safety properties of hybrid systems with neural network controllers. arXiv preprint arXiv:1811.01828 (2018)."},{"key":"e_1_2_1_25_1","volume-title":"Reluplex: An efficient SMT solver for verifying deep neural networks. In International Conference on Computer Aided Verification","author":"Katz G.","year":"2017","unstructured":"G. Katz , C. Barrett , D. L. Dill , K. Julian , and M. J. Kochenderfer . 2017 . Reluplex: An efficient SMT solver for verifying deep neural networks. In International Conference on Computer Aided Verification . Springer , 97--117. G. Katz, C. Barrett, D. L. Dill, K. Julian, and M. J. Kochenderfer. 2017. Reluplex: An efficient SMT solver for verifying deep neural networks. In International Conference on Computer Aided Verification. Springer, 97--117."},{"key":"e_1_2_1_26_1","volume-title":"Proc. of TACAS\u201915 (LNCS)","volume":"9035","author":"Kong S.","unstructured":"S. Kong , S. Gao , W. Chen , and E. M. Clarke . 2015. dReach: \u0394-reachability analysis for hybrid systems . In Proc. of TACAS\u201915 (LNCS) , Vol. 9035 . Springer, 200--205. S. Kong, S. Gao, W. Chen, and E. M. Clarke. 2015. dReach: \u0394-reachability analysis for hybrid systems. In Proc. of TACAS\u201915 (LNCS), Vol. 9035. Springer, 200--205."},{"key":"e_1_2_1_27_1","volume-title":"Continuous control with deep reinforcement learning. CoRR abs\/1509.02971","author":"Lillicrap Timothy P.","year":"2016","unstructured":"Timothy P. Lillicrap , Jonathan J. Hunt , Alexander Pritzel , Nicolas Heess , Tom Erez , Yuval Tassa , David Silver , and Daan Wierstra . 2016. Continuous control with deep reinforcement learning. CoRR abs\/1509.02971 ( 2016 ). Timothy P. Lillicrap, Jonathan J. Hunt, Alexander Pritzel, Nicolas Heess, Tom Erez, Yuval Tassa, David Silver, and Daan Wierstra. 2016. Continuous control with deep reinforcement learning. CoRR abs\/1509.02971 (2016)."},{"key":"e_1_2_1_28_1","unstructured":"George G. Lorentz. 2013. Bernstein Polynomials. American Mathematical Soc.  George G. Lorentz. 2013. Bernstein Polynomials. American Mathematical Soc."},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0005-1098(98)00193-9"},{"key":"e_1_2_1_30_1","first-page":"1611","article-title":"Verified global optimization with taylor model-based range bounders","volume":"11","author":"Makino K.","year":"2005","unstructured":"K. Makino and M. Berz . 2005 . Verified global optimization with taylor model-based range bounders . Transactions on Computers 11 , 4 (2005), 1611 -- 1618 . K. Makino and M. Berz. 2005. Verified global optimization with taylor model-based range bounders. Transactions on Computers 11, 4 (2005), 1611--1618.","journal-title":"Transactions on Computers"},{"key":"e_1_2_1_31_1","volume-title":"Differential Dynamical Systems","author":"Meiss J. D.","unstructured":"J. D. Meiss . 2007. Differential Dynamical Systems . SIAM publishers. J. D. Meiss. 2007. Differential Dynamical Systems. SIAM publishers."},{"key":"e_1_2_1_32_1","doi-asserted-by":"crossref","unstructured":"Volodymyr Mnih Koray Kavukcuoglu David Silver Andrei A. Rusu Joel Veness Marc G. Bellemare Alex Graves Martin Riedmiller Andreas K. Fidjeland Georg Ostrovski etal 2015. Human-level control through deep reinforcement learning. Nature 518 7540 (2015) 529.  Volodymyr Mnih Koray Kavukcuoglu David Silver Andrei A. Rusu Joel Veness Marc G. Bellemare Alex Graves Martin Riedmiller Andreas K. Fidjeland Georg Ostrovski et al. 2015. Human-level control through deep reinforcement learning. Nature 518 7540 (2015) 529.","DOI":"10.1038\/nature14236"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.15607\/RSS.2018.XIV.056"},{"key":"e_1_2_1_34_1","doi-asserted-by":"crossref","unstructured":"S. Prajna and A. Jadbabaie. 2004. Safety verification of hybrid systems using barrier certificates. In HSCC. Springer 477--492.  S. Prajna and A. Jadbabaie. 2004. Safety verification of hybrid systems using barrier certificates. In HSCC. Springer 477--492.","DOI":"10.1007\/978-3-540-24743-2_32"},{"key":"e_1_2_1_35_1","unstructured":"H. L. Royden. 1968. Real Analysis. Krishna Prakashan Media.  H. L. Royden. 1968. Real Analysis. Krishna Prakashan Media."},{"key":"e_1_2_1_36_1","doi-asserted-by":"crossref","unstructured":"W. Ruan X. Huang and M. Kwiatkowska. 2018. Reachability analysis of deep neural networks with provable guarantees. arXiv preprint arXiv:1805.02242 (2018).  W. Ruan X. Huang and M. Kwiatkowska. 2018. Reachability analysis of deep neural networks with provable guarantees. arXiv preprint arXiv:1805.02242 (2018).","DOI":"10.24963\/ijcai.2018\/368"},{"key":"e_1_2_1_37_1","volume-title":"Introduction to the Theory of Differential Inclusions","author":"Smirnov Georgi V.","unstructured":"Georgi V. Smirnov . 2002. Introduction to the Theory of Differential Inclusions . Vol. 41 . American Mathematical Soc . Georgi V. Smirnov. 2002. Introduction to the Theory of Differential Inclusions. Vol. 41. American Mathematical Soc."},{"key":"e_1_2_1_38_1","unstructured":"C. Szegedy W. Zaremba I. Sutskever J. Bruna D. Erhan I. Goodfellow and R. Fergus. 2013. Intriguing properties of neural networks. arXiv preprint arXiv:1312.6199 (2013).  C. Szegedy W. Zaremba I. Sutskever J. Bruna D. Erhan I. Goodfellow and R. Fergus. 2013. Intriguing properties of neural networks. arXiv preprint arXiv:1312.6199 (2013)."},{"key":"e_1_2_1_39_1","unstructured":"W. Xiang and T. T. Johnson. 2018. Reachability analysis and safety verification for neural network control systems. arXiv preprint arXiv:1805.09944 (2018).  W. Xiang and T. T. Johnson. 2018. Reachability analysis and safety verification for neural network control systems. arXiv preprint arXiv:1805.09944 (2018)."},{"key":"e_1_2_1_40_1","doi-asserted-by":"crossref","unstructured":"Z. Yang C. Huang X. Chen W. Lin and Z. Liu. 2016. A linear programming relaxation based approach for generating barrier certificates of hybrid systems. In FM. Springer 721--738.  Z. Yang C. Huang X. Chen W. Lin and Z. Liu. 2016. A linear programming relaxation based approach for generating barrier certificates of hybrid systems. In FM. Springer 721--738.","DOI":"10.1007\/978-3-319-48989-6_44"},{"key":"e_1_2_1_41_1","volume-title":"Spectral norm regularization for improving the generalizability of deep learning. arXiv preprint arXiv:1705.10941","author":"Yoshida Yuichi","year":"2017","unstructured":"Yuichi Yoshida and Takeru Miyato . 2017. Spectral norm regularization for improving the generalizability of deep learning. arXiv preprint arXiv:1705.10941 ( 2017 ). Yuichi Yoshida and Takeru Miyato. 2017. Spectral norm regularization for improving the generalizability of deep learning. arXiv preprint arXiv:1705.10941 (2017)."}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3358228","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3358228","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3358228","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:23:07Z","timestamp":1750188187000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3358228"}},"subtitle":["Reachability Analysis of Neural-Network Controlled Systems"],"short-title":[],"issued":{"date-parts":[[2019,10,8]]},"references-count":40,"journal-issue":{"issue":"5s","published-print":{"date-parts":[[2019,10,31]]}},"alternative-id":["10.1145\/3358228"],"URL":"https:\/\/doi.org\/10.1145\/3358228","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"value":"1539-9087","type":"print"},{"value":"1558-3465","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,10,8]]},"assertion":[{"value":"2019-04-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-07-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-10-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}