{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,13]],"date-time":"2026-01-13T15:53:15Z","timestamp":1768319595708,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":35,"publisher":"ACM","license":[{"start":{"date-parts":[[2023,5,9]],"date-time":"2023-05-09T00:00:00Z","timestamp":1683590400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2023,5,9]]},"DOI":"10.1145\/3575870.3587128","type":"proceedings-article","created":{"date-parts":[[2023,5,8]],"date-time":"2023-05-08T22:42:27Z","timestamp":1683585747000},"page":"1-13","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":11,"title":["Verification of Recurrent Neural Networks with Star Reachability"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6946-9526","authenticated-orcid":false,"given":"Hoang Dung","family":"Tran","sequence":"first","affiliation":[{"name":"University of Nebraska-Lincoln, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3679-5840","authenticated-orcid":false,"given":"Sung Woo","family":"Choi","sequence":"additional","affiliation":[{"name":"University of Nebraska-Lincoln, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1310-2615","authenticated-orcid":false,"given":"Xiaodong","family":"Yang","sequence":"additional","affiliation":[{"name":"Vanderbilt University, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0996-5725","authenticated-orcid":false,"given":"Tomoya","family":"Yamaguchi","sequence":"additional","affiliation":[{"name":"Woven Planet, Japan"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6255-7566","authenticated-orcid":false,"given":"Bardh","family":"Hoxha","sequence":"additional","affiliation":[{"name":"Toyota R & D, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6208-4233","authenticated-orcid":false,"given":"Danil","family":"Prokhorov","sequence":"additional","affiliation":[{"name":"Toyota R & D, USA"}]}],"member":"320","published-online":{"date-parts":[[2023,5,9]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v33i01.33016006"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63387-9_20"},{"key":"e_1_3_2_1_3_1","volume-title":"Improved Geometric Path Enumeration for Verifying ReLU Neural Networks. In 32nd International Conference on Computer Aided Verification. Springer.","author":"Bak Stanley","year":"2020","unstructured":"Stanley Bak, Hoang-Dung Tran, Kerianne Hobbs, and Taylor\u00a0T. Johnson. 2020. Improved Geometric Path Enumeration for Verifying ReLU Neural Networks. In 32nd International Conference on Computer Aided Verification. Springer."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/TASLP.2016.2598304"},{"key":"e_1_3_2_1_5_1","volume-title":"Life prediction of jet engines based on LSTM-recurrent neural networks. In 2017 Prognostics and system health management conference (PHM-Harbin)","author":"Dong Dong","unstructured":"Dong Dong, Xiao-Yang Li, and Fu-Qiang Sun. 2017. Life prediction of jet engines based on LSTM-recurrent neural networks. In 2017 Prognostics and system health management conference (PHM-Harbin). IEEE, 1\u20136."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41528-4_26"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-77935-5_9"},{"key":"e_1_3_2_1_8_1","volume-title":"Safety verification and robustness analysis of neural networks via quadratic constraints and semidefinite programming","author":"Fazlyab Mahyar","year":"2020","unstructured":"Mahyar Fazlyab, Manfred Morari, and George\u00a0J Pappas. 2020. Safety verification and robustness analysis of neural networks via quadratic constraints and semidefinite programming. IEEE Trans. Automat. Control (2020)."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-02165-7"},{"key":"e_1_3_2_1_10_1","volume-title":"A Neurosymbolic Approach to the Verification of Temporal Logic Properties of Learning enabled Control Systems. arXiv preprint arXiv:2303.05394","author":"Hashemi Navid","year":"2023","unstructured":"Navid Hashemi, Bardh Hoxha, Tomoya Yamaguchi, Danil Prokhorov, Geogios Fainekos, and Jyotirmoy Deshmukh. 2023. A Neurosymbolic Approach to the Verification of Temporal Logic Properties of Learning enabled Control Systems. arXiv preprint arXiv:2303.05394 (2023)."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.cosrev.2020.100270"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-59152-6_3"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63387-9_5"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_26"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81685-8_13"},{"key":"e_1_3_2_1_16_1","volume-title":"International Conference on Machine Learning. PMLR, 3468\u20133477","author":"Ko Ching-Yun","year":"2019","unstructured":"Ching-Yun Ko, Zhaoyang Lyu, Lily Weng, Luca Daniel, Ngai Wong, and Dahua Lin. 2019. POPQORN: Quantifying robustness of recurrent neural networks. In International Conference on Machine Learning. PMLR, 3468\u20133477."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1561\/9781680837872"},{"key":"e_1_3_2_1_18_1","volume-title":"Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence. 2873\u20132879","author":"Liu Pengfei","year":"2016","unstructured":"Pengfei Liu, Xipeng Qiu, and Xuanjing Huang. 2016. Recurrent neural network for text classification with multi-task learning. In Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence. 2873\u20132879."},{"key":"e_1_3_2_1_19_1","volume-title":"An approach to reachability analysis for feed-forward relu neural networks. arXiv preprint arXiv:1706.07351","author":"Lomuscio Alessio","year":"2017","unstructured":"Alessio Lomuscio and Lalit Maganti. 2017. An approach to reachability analysis for feed-forward relu neural networks. arXiv preprint arXiv:1706.07351 (2017)."},{"key":"e_1_3_2_1_20_1","first-page":"64","article-title":"Recurrent neural networks","volume":"5","author":"Medsker R","year":"2001","unstructured":"Larry\u00a0R Medsker and LC Jain. 2001. Recurrent neural networks. Design and Applications 5 (2001), 64\u201367.","journal-title":"Design and Applications"},{"key":"e_1_3_2_1_21_1","volume-title":"Distributed fault detection in sensor networks using a recurrent neural network. Neural processing letters 40, 3","author":"Obst Oliver","year":"2014","unstructured":"Oliver Obst. 2014. Distributed fault detection in sensor networks using a recurrent neural network. Neural processing letters 40, 3 (2014), 261\u2013273."},{"key":"e_1_3_2_1_22_1","volume-title":"Abstraction based output range analysis for neural networks. Advances in Neural Information Processing Systems 32","author":"Prabhakar Pavithra","year":"2019","unstructured":"Pavithra Prabhakar and Zahra Rahimi\u00a0Afzal. 2019. Abstraction based output range analysis for neural networks. Advances in Neural Information Processing Systems 32 (2019)."},{"key":"e_1_3_2_1_23_1","volume-title":"Fast and effective robustness certification for recurrent neural networks. CoRR abs\/2005.13300","author":"Ryou Wonryong","year":"2020","unstructured":"Wonryong Ryou, Jiayu Chen, Mislav Balunovic, Gagandeep Singh, Andrei\u00a0Marian Dan, and Martin\u00a0T Vechev. 2020. Fast and effective robustness certification for recurrent neural networks. CoRR abs\/2005.13300 (2020)."},{"key":"e_1_3_2_1_24_1","unstructured":"Gagandeep Singh Timon Gehr Matthew Mirman Markus P\u00fcschel and Martin Vechev. 2018. Fast and effective robustness certification. In Advances in Neural Information Processing Systems. 10825\u201310836."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290354"},{"key":"e_1_3_2_1_26_1","volume-title":"Verification of Deep Convolutional Neural Networks Using ImageStars. In 32nd International Conference on Computer-Aided Verification (CAV). Springer.","author":"Tran Hoang-Dung","year":"2020","unstructured":"Hoang-Dung Tran, Stanley Bak, Weiming Xiang, and Taylor\u00a0T. Johnson. 2020. Verification of Deep Convolutional Neural Networks Using ImageStars. In 32nd International Conference on Computer-Aided Verification (CAV). Springer."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/FormaliSE.2019.00012"},{"key":"e_1_3_2_1_28_1","volume-title":"23rd International Symposisum on Formal Methods (FM\u201919)","author":"Tran Hoang-Dung","year":"2019","unstructured":"Hoang-Dung Tran, Patrick Musau, Diego\u00a0Manzanas Lopez, Xiaodong Yang, Luan\u00a0Viet Nguyen, Weiming Xiang, and Taylor\u00a0T. Johnson. 2019. Star-Based Reachability Analsysis for Deep Neural Networks. In 23rd International Symposisum on Formal Methods (FM\u201919). Springer International Publishing."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-021-00553-4"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81685-8_12"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.5555\/AAI28288437"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53288-8_1"},{"key":"e_1_3_2_1_33_1","volume-title":"Verification for machine learning, autonomy, and neural networks survey. arXiv preprint arXiv:1810.01989","author":"Xiang Weiming","year":"2018","unstructured":"Weiming Xiang, Patrick Musau, Ayana\u00a0A Wild, Diego\u00a0Manzanas Lopez, Nathaniel Hamilton, Xiaodong Yang, Joel Rosenfeld, and Taylor\u00a0T Johnson. 2018. Verification for machine learning, autonomy, and neural networks survey. arXiv preprint arXiv:1810.01989 (2018)."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"crossref","unstructured":"Xiaodong Yang Taylor\u00a0T Johnson Hoang-Dung Tran Tomoya Yamaguchi Bardh Hoxha and Danil\u00a0V Prokhorov. 2021. Reachability analysis of deep ReLU neural networks using facet-vertex incidence.. In HSCC. 18\u20131.","DOI":"10.1145\/3447928.3456650"},{"key":"e_1_3_2_1_35_1","volume-title":"ECAI","author":"Zhang Hongce","year":"2020","unstructured":"Hongce Zhang, Maxwell Shinn, Aarti Gupta, Arie Gurfinkel, Nham Le, and Nina Narodytska. 2020. Verification of recurrent neural networks for cognitive tasks via reachability analysis. In ECAI 2020. IOS Press, 1690\u20131697."}],"event":{"name":"HSCC '23: 26th ACM International Conference on Hybrid Systems: Computation and Control","location":"San Antonio TX USA","acronym":"HSCC '23","sponsor":["SIGBED ACM Special Interest Group on Embedded Systems"]},"container-title":["Proceedings of the 26th ACM International Conference on Hybrid Systems: Computation and Control"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3575870.3587128","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3575870.3587128","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:46:12Z","timestamp":1750178772000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3575870.3587128"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,5,9]]},"references-count":35,"alternative-id":["10.1145\/3575870.3587128","10.1145\/3575870"],"URL":"https:\/\/doi.org\/10.1145\/3575870.3587128","relation":{},"subject":[],"published":{"date-parts":[[2023,5,9]]},"assertion":[{"value":"2023-05-09","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}