{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,3]],"date-time":"2026-06-03T16:58:28Z","timestamp":1780505908072,"version":"3.54.1"},"reference-count":52,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2020,12,7]],"date-time":"2020-12-07T00:00:00Z","timestamp":1607299200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100006602","name":"Air Force Research Laboratory","doi-asserted-by":"crossref","award":["FA8750-18-C-0090"],"award-info":[{"award-number":["FA8750-18-C-0090"]}],"id":[{"id":"10.13039\/100006602","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Embed. Comput. Syst."],"published-print":{"date-parts":[[2021,1,31]]},"abstract":"<jats:p>This article addresses the problem of verifying the safety of autonomous systems with neural network (NN) controllers. We focus on NNs with sigmoid\/tanh activations and use the fact that the sigmoid\/tanh is the solution to a quadratic differential equation. This allows us to convert the NN into an equivalent hybrid system and cast the problem as a hybrid system verification problem, which can be solved by existing tools. Furthermore, we improve the scalability of the proposed method by approximating the sigmoid with a Taylor series with worst-case error bounds. Finally, we provide an evaluation over four benchmarks, including comparisons with alternative approaches based on mixed integer linear programming as well as on star sets.<\/jats:p>","DOI":"10.1145\/3419742","type":"journal-article","created":{"date-parts":[[2020,12,7]],"date-time":"2020-12-07T18:26:48Z","timestamp":1607365608000},"page":"1-26","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":38,"title":["Verifying the Safety of Autonomous Systems with Neural Network Controllers"],"prefix":"10.1145","volume":"20","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4987-4836","authenticated-orcid":false,"given":"Radoslav","family":"Ivanov","sequence":"first","affiliation":[{"name":"University of Pennsylvania, Philadelphia, Pennsylvania"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Taylor J.","family":"Carpenter","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, Philadelphia, Pennsylvania"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"James","family":"Weimer","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, Philadelphia, Pennsylvania"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Rajeev","family":"Alur","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, Philadelphia, Pennsylvania"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"George J.","family":"Pappas","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, Philadelphia, Pennsylvania"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Insup","family":"Lee","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, Philadelphia, Pennsylvania"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2020,12,7]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"[n.d.]. F1\/10 Autonomous Racing Competition. Retrieved from http:\/\/f1tenth.org.  [n.d.]. F1\/10 Autonomous Racing Competition. Retrieved from http:\/\/f1tenth.org."},{"key":"e_1_2_1_2_1","volume-title":"Proceedings of the Workshop on Applied Verification for Continuous and Hybrid Systems. 120--151","author":"Althoff M.","year":"2015","unstructured":"M. Althoff . 2015 . An introduction to CORA 2015 . In Proceedings of the Workshop on Applied Verification for Continuous and Hybrid Systems. 120--151 . M. Althoff. 2015. An introduction to CORA 2015. In Proceedings of the Workshop on Applied Verification for Continuous and Hybrid Systems. 120--151."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00202-T"},{"key":"e_1_2_1_4_1","first-page":"07316","article-title":"End to end learning for self-driving cars","volume":"1604","author":"Bojarski M.","year":"2016","unstructured":"M. Bojarski , D. Del Testa , D. Dworakowski , B. Firner , B. Flepp , P. Goyal , L. D. Jackel , M. Monfort , U. Muller , J. Zhang , X. Zhang , and J. Zhao . 2016 . End to end learning for self-driving cars . ArXiv : 1604 . 07316 . Retrieved from https:\/\/arxiv.org\/abs\/1604.07316. M. Bojarski, D. Del Testa, D. Dworakowski, B. Firner, B. Flepp, P. Goyal, L. D. Jackel, M. Monfort, U. Muller, J. Zhang, X. Zhang, and J. Zhao. 2016. End to end learning for self-driving cars. ArXiv:1604.07316. Retrieved from https:\/\/arxiv.org\/abs\/1604.07316.","journal-title":"ArXiv"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/RTSS.2012.70"},{"key":"e_1_2_1_6_1","volume-title":"Proceedings of the International Conference on Computer Aided Verification. Springer, 258--263","author":"Chen X.","unstructured":"X. Chen , E. \u00c1brah\u00e1m , and S. Sankaranarayanan . 2013. Flow*: An analyzer for non-linear hybrid systems . In Proceedings of the International Conference on Computer Aided Verification. Springer, 258--263 . X. Chen, E. \u00c1brah\u00e1m, and S. Sankaranarayanan. 2013. Flow*: An analyzer for non-linear hybrid systems. In Proceedings of the International Conference on Computer Aided Verification. Springer, 258--263."},{"key":"e_1_2_1_7_1","volume-title":"Proceedings of the 34th International Conference on Machine Learning","volume":"70","author":"Cisse M.","unstructured":"M. Cisse , P. Bojanowski , E. Grave , Y. Dauphin , and N. Usunier . 2017. Parseval networks: Improving robustness to adversarial examples . In Proceedings of the 34th International Conference on Machine Learning , Vol. 70 . 854--863. M. Cisse, P. Bojanowski, E. Grave, Y. Dauphin, and N. Usunier. 2017. Parseval networks: Improving robustness to adversarial examples. In Proceedings of the 34th International Conference on Machine Learning, Vol. 70. 854--863."},{"key":"e_1_2_1_8_1","volume-title":"Natural language processing (almost) from scratch. J. Mach. Learn. Res. 12 (August","author":"Collobert Ronan","year":"2011","unstructured":"Ronan Collobert , Jason Weston , L\u00e9on Bottou , Michael Karlen , Koray Kavukcuoglu , and Pavel Kuksa . 2011. Natural language processing (almost) from scratch. J. Mach. Learn. Res. 12 (August 2011 ), 2493--2537. Ronan Collobert, Jason Weston, L\u00e9on Bottou, Michael Karlen, Koray Kavukcuoglu, and Pavel Kuksa. 2011. Natural language processing (almost) from scratch. J. Mach. Learn. Res. 12 (August 2011), 2493--2537."},{"key":"e_1_2_1_9_1","volume-title":"Proceedings of the NASA Formal Methods Symposium. Springer, 357--372","author":"Dreossi T.","unstructured":"T. Dreossi , A. Donz\u00e9 , and S. A. Seshia . 2017. Compositional falsification of cyber-physical systems with machine learning components . In Proceedings of the NASA Formal Methods Symposium. Springer, 357--372 . T. Dreossi, A. Donz\u00e9, and S. A. Seshia. 2017. Compositional falsification of cyber-physical systems with machine learning components. In Proceedings of the NASA Formal Methods Symposium. Springer, 357--372."},{"key":"e_1_2_1_10_1","volume-title":"Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 68--82","author":"Duggirala P. S.","unstructured":"P. S. Duggirala , S. Mitra , M. Viswanathan , and M. Potok . 2015. C2E2: A verification tool for stateflow models . In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 68--82 . P. S. Duggirala, S. Mitra, M. Viswanathan, and M. Potok. 2015. C2E2: A verification tool for stateflow models. In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 68--82."},{"key":"e_1_2_1_11_1","volume-title":"Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control. ACM, 157--168","author":"Dutta S.","unstructured":"S. Dutta , X. Chen , and S. Sankaranarayanan . 2019. Reachability analysis for neural feedback systems using regressive polynomial rule inference . In Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control. ACM, 157--168 . S. Dutta, X. Chen, and S. Sankaranarayanan. 2019. Reachability analysis for neural feedback systems using regressive polynomial rule inference. In Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control. ACM, 157--168."},{"key":"e_1_2_1_12_1","volume-title":"Proceedings of the 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 Proceedings of the 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 Proceedings of the NASA Formal Methods Symposium. Springer, 121--138."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-68167-2_19"},{"key":"e_1_2_1_14_1","volume-title":"Proceedings of the IEEE Conference on Computer Vision and Pattern Recognition. 1625--1634","author":"Eykholt K.","unstructured":"K. Eykholt , I. Evtimov , E. Fernandes , B. Li , A. Rahmati , C. Xiao , A. Prakash , T. Kohno , and D. Song . 2018. Robust physical-world attacks on deep learning visual classification . In Proceedings of the IEEE Conference on Computer Vision and Pattern Recognition. 1625--1634 . K. Eykholt, I. Evtimov, E. Fernandes, B. Li, A. Rahmati, C. Xiao, A. Prakash, T. Kohno, and D. Song. 2018. Robust physical-world attacks on deep learning visual classification. In Proceedings of the IEEE Conference on Computer Vision and Pattern Recognition. 1625--1634."},{"key":"e_1_2_1_15_1","first-page":"04893","article-title":"Efficient and accurate estimation of lipschitz constants for deep neural networks","volume":"1906","author":"Fazlyab Mahyar","year":"2019","unstructured":"Mahyar Fazlyab , Alexander Robey , Hamed Hassani , Manfred Morari , and George J. Pappas . 2019 . Efficient and accurate estimation of lipschitz constants for deep neural networks . ArXiv : 1906 . 04893 . Retrieved from https:\/\/arxiv.org\/abs\/1906.04893. Mahyar Fazlyab, Alexander Robey, Hamed Hassani, Manfred Morari, and George J. Pappas. 2019. Efficient and accurate estimation of lipschitz constants for deep neural networks. ArXiv:1906.04893. Retrieved from https:\/\/arxiv.org\/abs\/1906.04893.","journal-title":"ArXiv"},{"key":"e_1_2_1_16_1","volume-title":"Proceedings of the International Conference on Computer Aided Verification. 379--395","author":"Frehse G.","unstructured":"G. Frehse , C. L. 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 Proceedings of the International Conference on Computer Aided Verification. 379--395 . G. Frehse, C. L. 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 Proceedings of the International Conference on Computer Aided Verification. 379--395."},{"key":"e_1_2_1_17_1","first-page":"09477","article-title":"Addressing function approximation error in actor-critic methods","volume":"1802","author":"Fujimoto Scott","year":"2018","unstructured":"Scott Fujimoto , Herke van Hoof , and David Meger . 2018 . Addressing function approximation error in actor-critic methods . ArXiv : 1802 . 09477 . Retrieved from https:\/\/arxiv.org\/abs\/1802.09477. Scott Fujimoto, Herke van Hoof, and David Meger. 2018. Addressing function approximation error in actor-critic methods. ArXiv:1802.09477. Retrieved from https:\/\/arxiv.org\/abs\/1802.09477.","journal-title":"ArXiv"},{"key":"e_1_2_1_18_1","volume-title":"Proceedings of the IEEE Symposium on Security and Privacy (SP\u201918)","author":"Gehr T.","unstructured":"T. Gehr , M. Mirman , D. Drachsler-Cohen , P. Tsankov , S. Chaudhuri , and M. Vechev . 2018. AI2: Safety and robustness certification of neural networks with abstract interpretation . In Proceedings of the IEEE Symposium on Security and Privacy (SP\u201918) . T. Gehr, M. Mirman, D. Drachsler-Cohen, P. Tsankov, S. Chaudhuri, and M. Vechev. 2018. AI2: Safety and robustness certification of neural networks with abstract interpretation. In Proceedings of the IEEE Symposium on Security and Privacy (SP\u201918)."},{"key":"e_1_2_1_19_1","unstructured":"Matthias Hein and Maksym Andriushchenko. 2017. Formal guarantees on the robustness of a classifier against adversarial manipulation. In Advances in Neural Information Processing Systems. 2266--2276.  Matthias Hein and Maksym Andriushchenko. 2017. Formal guarantees on the robustness of a classifier against adversarial manipulation. In Advances in Neural Information Processing Systems. 2266--2276."},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3358228"},{"key":"e_1_2_1_21_1","volume-title":"Proceedings of the 23rd International Conference on Hybrid Systems: Computation and Control. ACM, 1--7.","author":"Ivanov R.","unstructured":"R. Ivanov , T. Carpenter , J. Weimer , R. Alur , G. J. Pappas , and I. Lee . 2020. Case study: Verifying the safety of an autonomous racing car with a neural network controller . In Proceedings of the 23rd International Conference on Hybrid Systems: Computation and Control. ACM, 1--7. R. Ivanov, T. Carpenter, J. Weimer, R. Alur, G. J. Pappas, and I. Lee. 2020. Case study: Verifying the safety of an autonomous racing car with a neural network controller. In Proceedings of the 23rd International Conference on Hybrid Systems: Computation and Control. ACM, 1--7."},{"key":"e_1_2_1_22_1","volume-title":"Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control. ACM, 169--178","author":"Ivanov R.","unstructured":"R. Ivanov , J. Weimer , R. Alur , G. J. Pappas , and I. Lee . 2019. Verisig: Verifying safety properties of hybrid systems with neural network controllers . In Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control. ACM, 169--178 . R. Ivanov, J. Weimer, R. Alur, G. J. Pappas, and I. Lee. 2019. Verisig: Verifying safety properties of hybrid systems with neural network controllers. In Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control. ACM, 169--178."},{"key":"e_1_2_1_23_1","volume-title":"Proceedings of the 2016 IEEE\/AIAA 35th Digital Avionics Systems Conference (DASC\u201916)","author":"Julian K. D.","unstructured":"K. D. Julian , J. Lopez , J. S. Brush , M. P. Owen , and M. J. Kochenderfer . 2016. Policy compression for aircraft collision avoidance systems . In Proceedings of the 2016 IEEE\/AIAA 35th Digital Avionics Systems Conference (DASC\u201916) . IEEE, 1--10. K. D. Julian, J. Lopez, J. S. Brush, M. P. Owen, and M. J. Kochenderfer. 2016. Policy compression for aircraft collision avoidance systems. In Proceedings of the 2016 IEEE\/AIAA 35th Digital Avionics Systems Conference (DASC\u201916). IEEE, 1--10."},{"key":"e_1_2_1_24_1","volume-title":"Reluplex: An efficient SMT solver for verifying deep neural networks. In Proceedings of the 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 Proceedings of the 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 Proceedings of the International Conference on Computer Aided Verification. Springer, 97--117."},{"key":"e_1_2_1_25_1","volume-title":"Proceedings of the International Conference on TOOLS and Algorithms for the Construction and Analysis of Systems. Springer, 200--205","author":"Kong S.","unstructured":"S. Kong , S. Gao , W. Chen , and E. Clarke . 2015. dReach: -reachability analysis for hybrid systems . In Proceedings of the International Conference on TOOLS and Algorithms for the Construction and Analysis of Systems. Springer, 200--205 . S. Kong, S. Gao, W. Chen, and E. Clarke. 2015. dReach: -reachability analysis for hybrid systems. In Proceedings of the International Conference on TOOLS and Algorithms for the Construction and Analysis of Systems. Springer, 200--205."},{"key":"e_1_2_1_26_1","first-page":"02533","article-title":"Adversarial examples in the physical world","volume":"1607","author":"Kurakin A.","year":"2016","unstructured":"A. Kurakin , I. Goodfellow , and S. Bengio . 2016 . Adversarial examples in the physical world . ArXiv : 1607 . 02533 . Retrieved from https:\/\/arxiv.org\/abs\/1607.02533. A. Kurakin, I. Goodfellow, and S. Bengio. 2016. Adversarial examples in the physical world. ArXiv:1607.02533. Retrieved from https:\/\/arxiv.org\/abs\/1607.02533.","journal-title":"ArXiv"},{"key":"e_1_2_1_27_1","volume-title":"Proceedings of the International Workshop on Hybrid Systems: Computation and Control. 137--151","author":"Lafferriere G.","unstructured":"G. Lafferriere , G. J. Pappas , and S. Yovine . 1999. A new class of decidable hybrid systems . In Proceedings of the International Workshop on Hybrid Systems: Computation and Control. 137--151 . G. Lafferriere, G. J. Pappas, and S. Yovine. 1999. A new class of decidable hybrid systems. In Proceedings of the International Workshop on Hybrid Systems: Computation and Control. 137--151."},{"key":"e_1_2_1_28_1","first-page":"02971","article-title":"Continuous control with deep reinforcement learning","volume":"1509","author":"Lillicrap T. P.","year":"2015","unstructured":"T. P. Lillicrap , J. J. Hunt , A. Pritzel , N. Heess , T. Erez , Y. Tassa , D. Silver , and D. Wierstra . 2015 . Continuous control with deep reinforcement learning . ArXiv : 1509 . 02971 . Retrieved from https:\/\/arxiv.org\/abs\/1509.02971. T. P. Lillicrap, J. J. Hunt, A. Pritzel, N. Heess, T. Erez, Y. Tassa, D. Silver, and D. Wierstra. 2015. Continuous control with deep reinforcement learning. ArXiv:1509.02971. Retrieved from https:\/\/arxiv.org\/abs\/1509.02971.","journal-title":"ArXiv"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.29007\/rgv8"},{"key":"e_1_2_1_30_1","first-page":"06083","article-title":"Towards deep learning models resistant to adversarial attacks","volume":"1706","author":"Madry Aleksander","year":"2017","unstructured":"Aleksander Madry , Aleksandar Makelov , Ludwig Schmidt , Dimitris Tsipras , and Adrian Vladu . 2017 . Towards deep learning models resistant to adversarial attacks . ArXiv : 1706 . 06083 . Retrieved from https:\/\/arxiv.org\/abs\/1706.06083. Aleksander Madry, Aleksandar Makelov, Ludwig Schmidt, Dimitris Tsipras, and Adrian Vladu. 2017. Towards deep learning models resistant to adversarial attacks. ArXiv:1706.06083. Retrieved from https:\/\/arxiv.org\/abs\/1706.06083.","journal-title":"ArXiv"},{"key":"e_1_2_1_31_1","first-page":"175","article-title":"Suppression of the wrapping effect by Taylor model-based verified integrators: The single step","volume":"36","author":"Makino Kyoko","year":"2007","unstructured":"Kyoko Makino and Martin Berz . 2007 . Suppression of the wrapping effect by Taylor model-based verified integrators: The single step . Int. J. Pure Appl. Math. 36 , 2 (2007), 175 . Kyoko Makino and Martin Berz. 2007. Suppression of the wrapping effect by Taylor model-based verified integrators: The single step. Int. J. Pure Appl. Math. 36, 2 (2007), 175.","journal-title":"Int. J. Pure Appl. Math."},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0893-6080(05)80129-7"},{"key":"e_1_2_1_33_1","volume-title":"Proceedings of the International Conference on Machine Learning. 3575--3583","author":"Mirman Matthew","year":"2018","unstructured":"Matthew Mirman , Timon Gehr , and Martin Vechev . 2018 . Differentiable abstract interpretation for provably robust neural networks . In Proceedings of the International Conference on Machine Learning. 3575--3583 . Matthew Mirman, Timon Gehr, and Martin Vechev. 2018. Differentiable abstract interpretation for provably robust neural networks. In Proceedings of the International Conference on Machine Learning. 3575--3583."},{"key":"e_1_2_1_35_1","unstructured":"OpenAI. [n.d.]. OpenAI Gym. Retrieved from https:\/\/gym.openai.com.  OpenAI. [n.d.]. OpenAI Gym. Retrieved from https:\/\/gym.openai.com."},{"key":"e_1_2_1_36_1","unstructured":"Gurobi Optimization. [n.d.]. Gurobi Optimizer. Retrieved from https:\/\/gurobi.com.  Gurobi Optimization. [n.d.]. Gurobi Optimizer. Retrieved from https:\/\/gurobi.com."},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132785"},{"key":"e_1_2_1_38_1","volume-title":"Proceedings of the Intelligent Vehicles Symposium. IEEE, 812--818","author":"Polack P.","unstructured":"P. Polack , F. Altch\u00e9 , B. d\u2019 Andr\u00e9a Novel , and A. de La Fortelle. 2017. The kinematic bicycle model: A consistent model for planning feasible trajectories for autonomous vehicles? . In Proceedings of the Intelligent Vehicles Symposium. IEEE, 812--818 . P. Polack, F. Altch\u00e9, B. d\u2019Andr\u00e9a Novel, and A. de La Fortelle. 2017. The kinematic bicycle model: A consistent model for planning feasible trajectories for autonomous vehicles?. In Proceedings of the Intelligent Vehicles Symposium. IEEE, 812--818."},{"key":"e_1_2_1_39_1","volume-title":"Vehicle Dynamics and Control","author":"Rajamani Rajesh","unstructured":"Rajesh Rajamani . 2011. Vehicle Dynamics and Control . Springer Science 8 Business Media. Rajesh Rajamani. 2011. Vehicle Dynamics and Control. Springer Science 8 Business Media."},{"key":"e_1_2_1_40_1","volume-title":"Le","author":"Ramachandran Prajit","year":"2017","unstructured":"Prajit Ramachandran , Barret Zoph , and Quoc V . Le . 2017 . Searching for activation functions. ArXiv:1710.05941 (2017). Retrieved from https:\/\/arxiv.org\/pdf\/1710.05941. Prajit Ramachandran, Barret Zoph, and Quoc V. Le. 2017. Searching for activation functions. ArXiv:1710.05941 (2017). Retrieved from https:\/\/arxiv.org\/pdf\/1710.05941."},{"key":"e_1_2_1_41_1","first-page":"03237","article-title":"Classification-based approximate reachability with guarantees applied to safe trajectory tracking","volume":"1803","author":"Royo V. R.","year":"2018","unstructured":"V. R. Royo , D. Fridovich-Keil , S. Herbert , and C. J. Tomlin . 2018 . Classification-based approximate reachability with guarantees applied to safe trajectory tracking . ArXiv : 1803 . 03237 . Retrieved from https:\/\/arxiv.org\/abs\/1803.03237. V. R. Royo, D. Fridovich-Keil, S. Herbert, and C. J. Tomlin. 2018. Classification-based approximate reachability with guarantees applied to safe trajectory tracking. ArXiv:1803.03237. Retrieved from https:\/\/arxiv.org\/abs\/1803.03237.","journal-title":"ArXiv"},{"key":"e_1_2_1_42_1","volume-title":"Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control. ACM, 147--156","author":"Sun X.","unstructured":"X. Sun , H. Khedr , and Y. Shoukry . 2019. Formal verification of neural network controlled autonomous systems . In Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control. ACM, 147--156 . X. Sun, H. Khedr, and Y. Shoukry. 2019. Formal verification of neural network controlled autonomous systems. In Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control. ACM, 147--156."},{"key":"e_1_2_1_43_1","first-page":"6199","article-title":"Intriguing properties of neural networks","volume":"1312","author":"Szegedy C.","year":"2013","unstructured":"C. Szegedy , W. Zaremba , I. Sutskever , J. Bruna , D. Erhan , et\u00a0al. 2013 . Intriguing properties of neural networks . ArXiv : 1312 . 6199 . Retrieved from https:\/\/arxiv.org\/abs\/1312.6199. C. Szegedy, W. Zaremba, I. Sutskever, J. Bruna, D. Erhan, et\u00a0al. 2013. Intriguing properties of neural networks. ArXiv:1312.6199. Retrieved from https:\/\/arxiv.org\/abs\/1312.6199.","journal-title":"ArXiv"},{"key":"e_1_2_1_44_1","volume-title":"Proceedings of the IEEE Conference on Computer Vision and Pattern Recognition. 1701--1708","author":"Taigman Y.","unstructured":"Y. Taigman , M. Yang , M. Ranzato , and L. Wolf . 2014. Deepface: Closing the gap to human-level performance in face verification . In Proceedings of the IEEE Conference on Computer Vision and Pattern Recognition. 1701--1708 . Y. Taigman, M. Yang, M. Ranzato, and L. Wolf. 2014. Deepface: Closing the gap to human-level performance in face verification. In Proceedings of the IEEE Conference on Computer Vision and Pattern Recognition. 1701--1708."},{"key":"e_1_2_1_45_1","volume-title":"Quantifier Elimination and Cylindrical Algebraic Decomposition","author":"Tarski A.","unstructured":"A. Tarski . 1998. A decision method for elementary algebra and geometry . In Quantifier Elimination and Cylindrical Algebraic Decomposition . Springer , 24--84. A. Tarski. 1998. A decision method for elementary algebra and geometry. In Quantifier Elimination and Cylindrical Algebraic Decomposition. Springer, 24--84."},{"key":"e_1_2_1_46_1","volume-title":"Proceedings of the 32nd International Conference on Computer-Aided Verification (CAV\u201920)","author":"Tran H.","unstructured":"H. Tran , S. Bak , W. Xiang , and T. T. Johnson . 2020. Verification of deep convolutional neural networks using ImageStars . In Proceedings of the 32nd International Conference on Computer-Aided Verification (CAV\u201920) . Springer. H. Tran, S. Bak, W. Xiang, and T. T. Johnson. 2020. Verification of deep convolutional neural networks using ImageStars. In Proceedings of the 32nd International Conference on Computer-Aided Verification (CAV\u201920). Springer."},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3358230"},{"key":"e_1_2_1_48_1","first-page":"06760","article-title":"Simulation-based adversarial test generation for autonomous vehicles with machine learning components","volume":"1804","author":"Tuncali Cumhur Erkan","year":"2018","unstructured":"Cumhur Erkan Tuncali , Georgios Fainekos , Hisahiro Ito , and James Kapinski . 2018 . Simulation-based adversarial test generation for autonomous vehicles with machine learning components . ArXiv : 1804 . 06760 . Retrieved from https:\/\/arxiv.org\/abs\/1804.06760. Cumhur Erkan Tuncali, Georgios Fainekos, Hisahiro Ito, and James Kapinski. 2018. Simulation-based adversarial test generation for autonomous vehicles with machine learning components. ArXiv:1804.06760. Retrieved from https:\/\/arxiv.org\/abs\/1804.06760.","journal-title":"ArXiv"},{"key":"e_1_2_1_49_1","unstructured":"S. Wang K. Pei J. Whitehouse J. Yang and S. Jana. 2018. Efficient formal safety analysis of neural networks. In Advances in Neural Information Processing Systems. 6367--6377.  S. Wang K. Pei J. Whitehouse J. Yang and S. Jana. 2018. Efficient formal safety analysis of neural networks. In Advances in Neural Information Processing Systems. 6367--6377."},{"key":"e_1_2_1_50_1","volume-title":"Proceedings of the International Conference on Machine Learning. 5273--5282","author":"Weng T.","unstructured":"T. Weng , H. Zhang , H. Chen , Z. Song , C. Hsieh , L. Daniel , D. Boning , and I. Dhillon . 2018. Towards fast computation of certified robustness for ReLU networks . In Proceedings of the International Conference on Machine Learning. 5273--5282 . T. Weng, H. Zhang, H. Chen, Z. Song, C. Hsieh, L. Daniel, D. Boning, and I. Dhillon. 2018. Towards fast computation of certified robustness for ReLU networks. In Proceedings of the International Conference on Machine Learning. 5273--5282."},{"key":"e_1_2_1_51_1","volume-title":"Algebraic Model Theory","author":"Wilkie A. J.","unstructured":"A. J. Wilkie . 1997. Schanuel\u2019s conjecture and the decidability of the real exponential field . In Algebraic Model Theory . Springer , 223--230. A. J. Wilkie. 1997. Schanuel\u2019s conjecture and the decidability of the real exponential field. In Algebraic Model Theory. Springer, 223--230."},{"key":"e_1_2_1_52_1","first-page":"01989","article-title":"Verification for machine learning, autonomy, and neural networks survey","volume":"1810","author":"Xiang W.","year":"2018","unstructured":"W. Xiang , P. Musau , A. A. Wild , D. M. Lopez , N. Hamilton , X. Yang , J. Rosenfeld , and T. T Johnson . 2018 . Verification for machine learning, autonomy, and neural networks survey . ArXiv : 1810 . 01989 . Retrieved from https:\/\/arxiv.org\/abs\/1810.01989. W. Xiang, P. Musau, A. A. Wild, D. M. Lopez, N. Hamilton, X. Yang, J. Rosenfeld, and T. T Johnson. 2018. Verification for machine learning, autonomy, and neural networks survey. ArXiv:1810.01989. Retrieved from https:\/\/arxiv.org\/abs\/1810.01989.","journal-title":"ArXiv"},{"key":"e_1_2_1_53_1","first-page":"03322","article-title":"Output reachable set estimation and verification for multi-layer neural networks","volume":"1708","author":"Xiang W.","year":"2017","unstructured":"W. Xiang , H. D. Tran , and T. T. Johnson . 2017 . Output reachable set estimation and verification for multi-layer neural networks . ArXiv : 1708 . 03322 . Retrieved from https:\/\/arxiv.org\/abs\/1708.03322. W. Xiang, H. D. Tran, and T. T. Johnson. 2017. Output reachable set estimation and verification for multi-layer neural networks. ArXiv:1708.03322. Retrieved from https:\/\/arxiv.org\/abs\/1708.03322.","journal-title":"ArXiv"}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3419742","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3419742","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T21:32:03Z","timestamp":1750195923000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3419742"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,12,7]]},"references-count":52,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2021,1,31]]}},"alternative-id":["10.1145\/3419742"],"URL":"https:\/\/doi.org\/10.1145\/3419742","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"value":"1539-9087","type":"print"},{"value":"1558-3465","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,12,7]]},"assertion":[{"value":"2020-02-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2020-08-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2020-12-07","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}