{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T02:40:07Z","timestamp":1774838407244,"version":"3.50.1"},"reference-count":40,"publisher":"Association for Computing Machinery (ACM)","issue":"4-5","license":[{"start":{"date-parts":[[2021,8,1]],"date-time":"2021-08-01T00:00:00Z","timestamp":1627776000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,8,1]],"date-time":"2021-08-01T00:00:00Z","timestamp":1627776000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2021,8]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Verification has emerged as a means to provide formal guarantees on\nlearning-based systems incorporating neural network before using\nthem in safety-critical applications. This paper proposes a new\nverification approach for deep neural networks (DNNs) with piecewise\nlinear activation functions using reachability analysis. The core of\nour approach is a collection of reachability algorithms using star\nsets (or shortly, stars), an effective symbolic representation of\nhigh-dimensional polytopes. The star-based reachability algorithms\ncompute the output reachable sets of a network with a given input\nset before using them for verification. For a neural network with\npiecewise linear activation functions, our approach can construct\nboth exact and over-approximate reachable sets of the neural\nnetwork. To enhance the scalability of our approach, a star set is\nequipped with an outer-zonotope (a zonotope over-approximation of\nthe star set) to quickly estimate the lower and upper bounds of an\ninput set at a specific neuron to determine if splitting occurs at\nthat neuron. This zonotope pre-filtering step reduces significantly\nthe number of linear programming optimization problems that\nmust be solved in the analysis, and leads to a reduction in\ncomputation time, which enhances the scalability of the star set\napproach. Our reachability algorithms are implemented in a software\nprototype called the neural network verification tool, and can\nbe applied to problems analyzing the robustness of machine learning\nmethods, such as safety and robustness verification of DNNs. Our\nexperiments show that our approach can achieve runtimes twenty to\n1400 times faster than Reluplex, a satisfiability modulo\ntheory-based approach. Our star set approach is also less\nconservative than other recent zonotope and abstract domain\napproaches.<\/jats:p>","DOI":"10.1007\/s00165-021-00553-4","type":"journal-article","created":{"date-parts":[[2021,8,28]],"date-time":"2021-08-28T03:27:55Z","timestamp":1630121275000},"page":"519-545","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":15,"title":["Verification of piecewise deep neural networks: a star set approach with zonotope pre-filter"],"prefix":"10.1145","volume":"33","author":[{"given":"Hoang-Dung","family":"Tran","sequence":"first","affiliation":[{"name":"University of Nebraska Lincoln, Lincoln, NE, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Neelanjana","family":"Pal","sequence":"additional","affiliation":[{"name":"Vanderbilt University, Nashville, TN, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Diego Manzanas","family":"Lopez","sequence":"additional","affiliation":[{"name":"Vanderbilt University, Nashville, TN, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Patrick","family":"Musau","sequence":"additional","affiliation":[{"name":"Vanderbilt University, Nashville, TN, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xiaodong","family":"Yang","sequence":"additional","affiliation":[{"name":"Vanderbilt University, Nashville, TN, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luan Viet","family":"Nguyen","sequence":"additional","affiliation":[{"name":"University of Dayton, Dayton, OH, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Weiming","family":"Xiang","sequence":"additional","affiliation":[{"name":"Augusta University, Augusta, GA, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stanley","family":"Bak","sequence":"additional","affiliation":[{"name":"Stony Brook University, Stony Brook, NY, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8021-9923","authenticated-orcid":false,"given":"Taylor T.","family":"Johnson","sequence":"additional","affiliation":[{"name":"Vanderbilt University, Nashville, TN, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Akintunde ME Kevorchian A Lomuscio A Pirovano E (2019) Verification of RNN-based neural agent-environment systems. In: Proceedings of the 33th AAAI conference on artificial intelligence (AAAI19). Honolulu HI USA. AAAI Press (to appear)","DOI":"10.1609\/aaai.v33i01.33016006"},{"key":"e_1_2_1_2_2_2","unstructured":"Akintunde M Lomuscio A Maganti L Pirovano E (2018) Reachability analysis for neural agent-environment systems. In:\nSixteenth international conference on principles of knowledge representation and reasoning"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Bak S Duggirala PS (2017) Simulation-equivalent reachability of large linear systems with inputs. In: International conference\non computer aided verification. Springer pp 401\u2013420","DOI":"10.1007\/978-3-319-63387-9_20"},{"key":"e_1_2_1_2_4_2","unstructured":"Bojarski M Del Testa D Dworakowski D Firner B Flepp B Goyal P Jackel LD Monfort M Muller U Zhang J et al (2016)\nEnd to end learning for self-driving cars. arXiv preprint arXiv:1604.07316"},{"key":"e_1_2_1_2_5_2","unstructured":"Bastani O Ioannou Y Lampropoulos L Vytiniotis D Nori A Criminisi A (2016) Measuring neural net robustness with\nconstraints. In: Advances in neural information processing systems pp 2613\u20132621"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Bak S Tran H-D Hobbs K Johnson T (2020) Improved geometric path enumeration for verifying ReLU neural networks. In:\nProceedings of the 32nd international conference on computer aided verification. Springer","DOI":"10.1007\/978-3-030-53288-8_4"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Dutta S Jha S Sanakaranarayanan S Tiwari A (2017) Output range analysis for deep neural networks. arXiv preprint arXiv:1709.09130","DOI":"10.1007\/978-3-319-77935-5_9"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Ehlers R (2017) Formal verification of piece-wise linear feed-forward neural networks. In: International symposium on automated\ntechnology for verification and analysis. Springer pp 269\u2013286","DOI":"10.1007\/978-3-319-68167-2_19"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Gehr T Mirman M Drachsler-Cohen D Tsankov P Chaudhuri S Vechev M (2018) Ai 2: safety and robustness certification\nof neural networks with abstract interpretation. In: 2018 IEEE symposium on security and privacy (SP)","DOI":"10.1109\/SP.2018.00058"},{"key":"e_1_2_1_2_10_2","unstructured":"Goodfellow IJ Shlens J Szegedy C (2014) Explaining and harnessing adversarial examples. arXiv preprint arXiv:1412.6572"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Hinton G Deng L Yu D Dahl GE Mohamed A Jaitly N Senior A Vanhoucke V Nguyen P Sainath TN et al (2012) Deep\nneural networks for acoustic modeling in speech recognition: the shared views of four research groups. IEEE Signal Process\nMag 29(6):82\u201397","DOI":"10.1109\/MSP.2012.2205597"},{"key":"e_1_2_1_2_12_2","unstructured":"Heilweil R (2020) Tesla needs to fix its deadly Autopilot problem"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Huang X Kwiatkowska M Wang S Wu M (2017) Safety verification of deep neural networks. In: International conference\non computer aided verification. Springer pp 3\u201329","DOI":"10.1007\/978-3-319-63387-9_1"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"Julian KD Kochenderfer MJ Owen MP (2018) Deep neural network compression for aircraft collision avoidance systems.\narXiv preprint arXiv:1810.04240","DOI":"10.2514\/1.G003724"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Katz G Barrett C Dill DL Julian K Kochenderfer MJ (2017) Reluplex: an efficient smt solver for verifying deep neural\nnetworks. In: International conference on computer aided verification. Springer pp 97\u2013117","DOI":"10.1007\/978-3-319-63387-9_5"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Kvasnica M Grieder P Baoti\u0107 M Morari M (2004) Multi-parametric toolbox (MPT). In: International workshop on hybrid\nsystems: computation and control. Springer pp 448\u2013462","DOI":"10.1007\/978-3-540-24743-2_30"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Guy K Derek AH Duligur I Kyle J Christopher L Rachel L Parth S Shantanu T Haoze W Aleksandar Z et al (2019) The\nmarabou framework for verification and analysis of deep neural networks. In: International conference on computer aided\nverification. Springer pp 443\u2013452","DOI":"10.1007\/978-3-030-25540-4_26"},{"key":"e_1_2_1_2_18_2","unstructured":"Kouvaros P Lomuscio A (2018) Formal verification of cnn-based perception systems. arXiv preprint arXiv:1811.11373"},{"key":"e_1_2_1_2_19_2","unstructured":"LeCun Y (1998) The mnist database of handwritten digits. http:\/\/yann.lecun.com\/exdb\/mnist\/"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","unstructured":"Litjens G Kooi T Bejnordi BE Setio AAA Ciompi F Ghafoorian M van der Laak Jeroen AWM Van Ginneken B S\u00e1nchez\nCI (2017) A survey on deep learning in medical image analysis. Med Image Anal 42:60\u201388","DOI":"10.1016\/j.media.2017.07.005"},{"key":"e_1_2_1_2_21_2","unstructured":"Lomuscio A Maganti L (2017) An approach to reachability analysis for feed-forward relu neural networks. arXiv preprint arXiv:1706.07351"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","unstructured":"Liu W Wang Z Liu X Zeng N Liu Y Alsaadi FE (2017) A survey of deep neural network architectures and their applications.\nNeurocomputing 234:11\u201326","DOI":"10.1016\/j.neucom.2016.12.038"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"crossref","unstructured":"Moosavi-Dezfooli S-M Fawzi A Frossard P (2016) Deepfool: a simple and accurate method to fool deep neural networks. In:\nProceedings of the IEEE conference on computer vision and pattern recognition pp 2574\u20132582","DOI":"10.1109\/CVPR.2016.282"},{"key":"e_1_2_1_2_24_2","unstructured":"Muoio D (2017) The self-driving Uber in the Arizona crash was hit crossing an intersection on yellowUber crashes"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"crossref","unstructured":"Pulina L Tacchella A (2010) An abstraction-refinement approach to verification of artificial neural networks. In: International\nconference on computer aided verification. Springer pp 243\u2013257","DOI":"10.1007\/978-3-642-14295-6_24"},{"key":"e_1_2_1_2_26_2","unstructured":"Singh G Gehr T Mirman M P\u00fcschel M Vechev M (2018) Fast and effective robustness certification. In: Advances in neural\ninformation processing systems pp 10825\u201310836"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"Singh G Gehr T P\u00fcschel M Vechev M (2019) An abstract domain for certifying neural networks. Proc ACM Programm Lang\n3(POPL):41","DOI":"10.1145\/3290354"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"crossref","unstructured":"Tran H-D Bak S Xiang W Johnson TT (2020) Verification of deep convolutional neural networks using imagestars. In: 32nd\ninternational conference on computer-aided verification (CAV). Springer","DOI":"10.1007\/978-3-030-53288-8_2"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","unstructured":"Tran H-D Musau P Lopez DM Yang X Nguyen LV Xiang W Johnson TT (2019) Parallelizable reachability analysis\nalgorithms for feed-forward neural networks. In: 7th international conference on formal methods in software engineering\n(FormaliSE2019) Montreal Canada","DOI":"10.1109\/FormaliSE.2019.00012"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"crossref","unstructured":"Tran H-D Musau P Lopez DM Yang X Nguyen LV Xiang W Johnson TT (2019) Star-based reachability analsysis for deep\nneural networks. In: 23rd international symposisum on formal methods (FM\u201919). Springer","DOI":"10.1007\/978-3-030-30942-8_39"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"crossref","unstructured":"Tran H-D Pal N Musau P Yang X Hamilton NP Lopez DM Bak S Johnson TT (2021) Robustness verification of semantic\nsegmentation neural networks using relaxed reachability. In: Proceedings of the 33rd international conference on computeraided\nverification. Springer","DOI":"10.1007\/978-3-030-81685-8_12"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"crossref","unstructured":"Tran H-D Yang X Lopez DM Musau P Nguyen LV Xiang W Bak S Johnson TT (2020) NNV: the neural network\nverification tool for deep neural networks and learning-enabled cyber-physical systems. In: 32nd international conference on\ncomputer-aided verification (CAV)","DOI":"10.1109\/DESTION50928.2020.00010"},{"key":"e_1_2_1_2_33_2","unstructured":"Wang S Pei K Whitehouse J Yang J Jana S (2018) Efficient formal safety analysis of neural networks. In: Advances in neural\ninformation processing systems pp 6369\u20136379"},{"key":"e_1_2_1_2_34_2","unstructured":"Wang S Pei K Whitehouse J Yang J Jana S (2018) Formal security analysis of neural networks using symbolic intervals.\narXiv preprint arXiv:1804.10829"},{"key":"e_1_2_1_2_35_2","unstructured":"Weng T-W Zhang H Chen H Song Z Hsieh C-J Boning D Dhillon IS Daniel L (2018) Towards fast computation of certified\nrobustness for relu networks. arXiv preprint arXiv:1804.09699"},{"key":"e_1_2_1_2_36_2","unstructured":"Xiang W Musau P Wild AA Lopez DM Hamilton N Yang X Rosenfeld JA Johnson TT (2018) Verification for machine\nlearning autonomy and neural networks survey. CoRR arXiv:1810.01989"},{"key":"e_1_2_1_2_37_2","unstructured":"Xiang W Tran H-D Johnson TT (2017) Reachable set computation and safety verification for neural networks with relu\nactivations. arXiv preprint arXiv:1712.08163"},{"key":"e_1_2_1_2_38_2","unstructured":"Xiang W Tran H-D Johnson TT (2018) Output reachable set estimation and verification formultilayer neural networks. IEEE\nTrans Neural Netw Learn Syst (99):1\u20137"},{"key":"e_1_2_1_2_39_2","unstructured":"Xiang W Tran H-D Johnson TT (2019) Specification-guided safety verification for feedforward neural networks. AAAI Spring\nsymposium on verification of neural networks"},{"key":"e_1_2_1_2_40_2","unstructured":"Zhang H Weng T-W Chen P-Y Hsieh C-J Daniel L (2018) Efficient neural network robustness certification with general\nactivation functions. In: Advances in neural information processing systems pp 4944\u20134953"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-021-00553-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00165-021-00553-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-021-00553-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-021-00553-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T16:25:28Z","timestamp":1641486328000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-021-00553-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,8]]},"references-count":40,"journal-issue":{"issue":"4-5","published-print":{"date-parts":[[2021,8]]}},"alternative-id":["10.1007\/s00165-021-00553-4"],"URL":"https:\/\/doi.org\/10.1007\/s00165-021-00553-4","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,8]]},"assertion":[{"value":"10 April 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"29 May 2021","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"28 August 2021","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}