{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:09:21Z","timestamp":1750219761478,"version":"3.41.0"},"reference-count":36,"publisher":"Association for Computing Machinery (ACM)","issue":"6","license":[{"start":{"date-parts":[[2023,10,16]],"date-time":"2023-10-16T00:00:00Z","timestamp":1697414400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"Doctoral College Resilient Embedded Systems"},{"name":"TU Wien\u2019s Faculty of Informatics and FH-Technikum Wien"},{"DOI":"10.13039\/501100011688","name":"ECSEL Joint Undertaking","doi-asserted-by":"crossref","award":["H2020-ECSEL-2019-IA-876190"],"award-info":[{"award-number":["H2020-ECSEL-2019-IA-876190"]}],"id":[{"id":"10.13039\/501100011688","id-type":"DOI","asserted-by":"crossref"}]},{"name":"NYUAD\u2019s Research Enhancement Fund"},{"name":"NYUAD Center for Artificial Intelligence and Robotics"},{"DOI":"10.13039\/100020770","name":"NYUAD Research Institute","doi-asserted-by":"crossref","award":["CG010"],"award-info":[{"award-number":["CG010"]}],"id":[{"id":"10.13039\/100020770","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Des. Autom. Electron. Syst."],"published-print":{"date-parts":[[2023,11,30]]},"abstract":"<jats:p>\n            Over the past years, numerous studies demonstrated the vulnerability of deep neural networks (DNNs) to make correct classifications in the presence of small noise. This motivated the formal analysis of DNNs to ensure that they delineate acceptable behavior. However, in the case that the DNN\u2019s behavior is unacceptable for the desired application, these\n            <jats:italic>qualitative<\/jats:italic>\n            approaches are ill equipped to determine the precise degree to which the DNN behaves unacceptably.\n          <\/jats:p>\n          <jats:p>\n            \u00a0\u00a0We propose a novel\n            <jats:italic>quantitative<\/jats:italic>\n            DNN analysis framework, QuanDA, which not only checks whether the DNN delineates certain behavior but also provides the estimated probability of the DNN to delineate this particular behavior. Unlike the (few) available quantitative DNN analysis frameworks, QuanDA does not use any implicit assumptions on the probability distribution of the hidden nodes, which enables the framework to propagate close to real probability distributions of the hidden node values to each proceeding DNN layer. Furthermore, our framework leverages CUDA to parallelize the analysis, enabling high-speed GPU implementation for fast analysis. The applicability of the framework is demonstrated using the ACAS Xu benchmark, to provide reachability probability estimates for all network nodes. This paper also provides potential applications of QuanDA for the analysis of DNN safety properties.\n          <\/jats:p>","DOI":"10.1145\/3611671","type":"journal-article","created":{"date-parts":[[2023,8,1]],"date-time":"2023-08-01T11:54:43Z","timestamp":1690890883000},"page":"1-21","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["QuanDA: GPU Accelerated Quantitative Deep Neural Network Analysis"],"prefix":"10.1145","volume":"28","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3096-9536","authenticated-orcid":false,"given":"Mahum","family":"Naseer","sequence":"first","affiliation":[{"name":"Institute of Computer Engineering, Vienna University of Technology, Austria"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2562-2669","authenticated-orcid":false,"given":"Osman","family":"Hasan","sequence":"additional","affiliation":[{"name":"School of Electrical Engineering &amp; Computer Science (SEECS), National University of Sciences &amp; Technology (NUST), Pakistan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2607-8135","authenticated-orcid":false,"given":"Muhammad","family":"Shafique","sequence":"additional","affiliation":[{"name":"Division of Engineering, New York University Abu Dhabi (NYUAD), United Arab Emirates"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,10,16]]},"reference":[{"issue":"1","key":"e_1_3_3_2_2","doi-asserted-by":"crossref","first-page":"189","DOI":"10.3758\/BF03342857","article-title":"Note on weighted sum and linear operator models","volume":"1","author":"Anderson Norman H.","year":"1964","unstructured":"Norman H. Anderson. 1964. Note on weighted sum and linear operator models. Psychonomic Science 1, 1 (1964), 189\u2013190.","journal-title":"Psychonomic Science"},{"key":"e_1_3_3_3_2","first-page":"2613","volume-title":"Advances in Neural Information Processing Systems","author":"Bastani Osbert","year":"2016","unstructured":"Osbert Bastani, Yani Ioannou, Leonidas Lampropoulos, Dimitrios Vytiniotis, Aditya Nori, and Antonio Criminisi. 2016. Measuring neural net robustness with constraints. In Advances in Neural Information Processing Systems. 2613\u20132621."},{"key":"e_1_3_3_4_2","volume-title":"AAAI Conference on Artificial Intelligence","author":"Botoeva Elena","year":"2020","unstructured":"Elena Botoeva, Panagiotis Kouvaros, Jan Kronqvist, Alessio Lomuscio, and Ruth Misener. 2020. Efficient verification of ReLU-based neural networks via dependency analysis. In AAAI Conference on Artificial Intelligence."},{"key":"e_1_3_3_5_2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1022483715767"},{"issue":"2020","key":"e_1_3_3_6_2","article-title":"Branch and bound for piecewise linear neural network verification","volume":"21","author":"Bunel Rudy","year":"2020","unstructured":"Rudy Bunel, Jingyue Lu, Ilker Turkaslan, P. Kohli, P. Torr, and P Mudigonda. 2020. Branch and bound for piecewise linear neural network verification. Journal of Machine Learning Research 21, 2020 (2020).","journal-title":"Journal of Machine Learning Research"},{"key":"e_1_3_3_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-03592-1_16"},{"key":"e_1_3_3_8_2","doi-asserted-by":"crossref","first-page":"148","DOI":"10.1109\/ISSRE5003.2020.00023","volume-title":"2020 IEEE 31st International Symposium on Software Reliability Engineering (ISSRE\u201920)","author":"Converse Hayes","year":"2020","unstructured":"Hayes Converse, Antonio Filieri, Divya Gopinath, and Corina S. P\u0103s\u0103reanu. 2020. Probabilistic symbolic analysis of neural networks. In 2020 IEEE 31st International Symposium on Software Reliability Engineering (ISSRE\u201920). IEEE, 148\u2013159."},{"key":"e_1_3_3_9_2","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1007\/978-3-319-77935-5_9","volume-title":"NASA Formal Methods Symposium","author":"Dutta Souradeep","year":"2018","unstructured":"Souradeep Dutta, Susmit Jha, Sriram Sankaranarayanan, and Ashish Tiwari. 2018. Output range analysis for deep feedforward neural networks. In NASA Formal Methods Symposium. Springer, 121\u2013138."},{"key":"e_1_3_3_10_2","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1007\/978-3-319-68167-2_19","volume-title":"International Symposium on Automated Technology for Verification and Analysis","author":"Ehlers Ruediger","year":"2017","unstructured":"Ruediger Ehlers. 2017. Formal verification of piece-wise linear feed-forward neural networks. In International Symposium on Automated Technology for Verification and Analysis. Springer, 269\u2013286."},{"key":"e_1_3_3_11_2","doi-asserted-by":"publisher","DOI":"10.1038\/s41591-018-0316-z"},{"key":"e_1_3_3_12_2","first-page":"770","volume-title":"IEEE CVPR","author":"al. Kaiming He et","year":"2016","unstructured":"Kaiming He et al.2016. Deep residual learning for image recognition. In IEEE CVPR. 770\u2013778."},{"key":"e_1_3_3_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/502102.502106"},{"key":"e_1_3_3_14_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0865-5_26"},{"key":"e_1_3_3_15_2","first-page":"4700","volume-title":"Computer Vision and Pattern Recognition","author":"Huang Gao","year":"2017","unstructured":"Gao Huang, Zhuang Liu, Laurens Van Der Maaten, and Kilian Q. Weinberger. 2017. Densely connected convolutional networks. In Computer Vision and Pattern Recognition. 4700\u20134708."},{"key":"e_1_3_3_16_2","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/978-3-319-63387-9_1","volume-title":"International Conference on Computer Aided Verification (CAV\u201917)","author":"Huang Xiaowei","year":"2017","unstructured":"Xiaowei Huang, Marta Kwiatkowska, Sen Wang, and Min Wu. 2017. Safety verification of deep neural networks. In International Conference on Computer Aided Verification (CAV\u201917). Springer, 3\u201329."},{"key":"e_1_3_3_17_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63387-9_5"},{"key":"e_1_3_3_18_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_26"},{"key":"e_1_3_3_19_2","first-page":"1","volume-title":"Proceedings of the 2nd Workshop on the LLVM Compiler Infrastructure in HPC","author":"Lam Siu Kwan","year":"2015","unstructured":"Siu Kwan Lam, Antoine Pitrou, and Stanley Seibert. 2015. Numba: A LLVM-based Python JIT compiler. In Proceedings of the 2nd Workshop on the LLVM Compiler Infrastructure in HPC. 1\u20136."},{"key":"e_1_3_3_20_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.knosys.2020.106617"},{"key":"e_1_3_3_21_2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3498704","article-title":"PRIMA: General and precise neural network certification via scalable convex hull approximations.","volume":"6","author":"M\u00fcller Mark Niklas","year":"2022","unstructured":"Mark Niklas M\u00fcller, Gleb Makarchuk, Gagandeep Singh, Markus P\u00fcschel, and Martin T. Vechev. 2022. PRIMA: General and precise neural network certification via scalable convex hull approximations. Proc. ACM Program. Lang. 6, POPL (2022), 1\u201333.","journal-title":"Proc. ACM Program. Lang."},{"key":"e_1_3_3_22_2","volume-title":"AAAI Conference on Artificial Intelligence","author":"Narodytska Nina","year":"2018","unstructured":"Nina Narodytska, Shiva Kasiviswanathan, Leonid Ryzhyk, Mooly Sagiv, and Toby Walsh. 2018. Verifying properties of binarized deep neural networks. In AAAI Conference on Artificial Intelligence."},{"key":"e_1_3_3_23_2","first-page":"666","volume-title":"Proc. DATE","author":"Naseer Mahum","year":"2020","unstructured":"Mahum Naseer, Mishal Fatima Minhas, Faiq Khalid, Muhammad Abdullah Hanif, Osman Hasan, and Muhammad Shafique. 2020. FANNet: Formal analysis of noise tolerance, training bias and input sensitivity in neural networks. In Proc. DATE. IEEE, 666\u2013669."},{"key":"e_1_3_3_24_2","first-page":"1","volume-title":"2019 IEEE\/AIAA 38th Digital Avionics Systems Conference (DASC\u201919)","author":"Owen Michael P.","year":"2019","unstructured":"Michael P. Owen, Adam Panken, Robert Moss, Luis Alvarez, and Charles Leeper. 2019. ACAS Xu: Integrated collision avoidance and detect and avoid capability for UAS. In 2019 IEEE\/AIAA 38th Digital Avionics Systems Conference (DASC\u201919). IEEE, 1\u201310."},{"key":"e_1_3_3_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132785"},{"key":"e_1_3_3_26_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10472-011-9243-0"},{"key":"e_1_3_3_27_2","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2019.2891969"},{"key":"e_1_3_3_28_2","first-page":"30","volume-title":"MBMV","author":"Scheibler Karsten","year":"2015","unstructured":"Karsten Scheibler, Leonore Winterer, Ralf Wimmer, and Bernd Becker. 2015. Towards verification of artificial neural networks. In MBMV. 30\u201340."},{"key":"e_1_3_3_29_2","volume-title":"AAAI Spring Symposium on Verification of Neural Networks (VNN\u201919)","author":"Shih Andy","year":"2019","unstructured":"Andy Shih, Adnan Darwiche, and Arthur Choi. 2019. Verifying binarized neural networks by local automaton learning. In AAAI Spring Symposium on Verification of Neural Networks (VNN\u201919)."},{"key":"e_1_3_3_30_2","first-page":"41","article-title":"An abstract domain for certifying neural networks","volume":"3","author":"Singh Gagandeep","year":"2019","unstructured":"Gagandeep Singh, Timon Gehr, Markus P\u00fcschel, and Martin Vechev. 2019. An abstract domain for certifying neural networks. Proceedings of the ACM on Programming Languages 3, POPL (2019), 41.","journal-title":"Proceedings of the ACM on Programming Languages"},{"key":"e_1_3_3_31_2","article-title":"QNNVerifier: A tool for verifying neural networks using SMT-based model checking","author":"Song Xidan","year":"2021","unstructured":"Xidan Song, Edoardo Manino, Luiz Sena, Erickson Alves, Iury Bessa, Mikel Lujan, Lucas Cordeiro, et\u00a0al. 2021. QNNVerifier: A tool for verifying neural networks using SMT-based model checking. arXiv preprint arXiv:2111.13110 (2021).","journal-title":"arXiv preprint arXiv:2111.13110"},{"key":"e_1_3_3_32_2","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2017.2761740"},{"key":"e_1_3_3_33_2","article-title":"Intriguing properties of neural networks","author":"Szegedy Christian","year":"2013","unstructured":"Christian Szegedy, Wojciech Zaremba, Ilya Sutskever, Joan Bruna, Dumitru Erhan, Ian Goodfellow, and Rob Fergus. 2013. Intriguing properties of neural networks. arXiv preprint arXiv:1312.6199 (2013).","journal-title":"arXiv preprint arXiv:1312.6199"},{"issue":"4","key":"e_1_3_3_34_2","doi-asserted-by":"crossref","first-page":"519","DOI":"10.1007\/s00165-021-00553-4","article-title":"Verification of piecewise deep neural networks: A star set approach with zonotope pre-filter","volume":"33","author":"Tran Hoang-Dung","year":"2021","unstructured":"Hoang-Dung Tran, Neelanjana Pal, Diego Manzanas Lopez, Patrick Musau, Xiaodong Yang, Luan Viet Nguyen, Weiming Xiang, Stanley Bak, and Taylor T. Johnson. 2021. Verification of piecewise deep neural networks: A star set approach with zonotope pre-filter. Formal Aspects of Computing 33, 4 (2021), 519\u2013545.","journal-title":"Formal Aspects of Computing"},{"key":"e_1_3_3_35_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10489-021-02728-1"},{"key":"e_1_3_3_36_2","first-page":"6367","volume-title":"Advances in Neural Information Processing Systems","author":"Wang Shiqi","year":"2018","unstructured":"Shiqi Wang, Kexin Pei, Justin Whitehouse, Junfeng Yang, and Suman Jana. 2018. Efficient formal safety analysis of neural networks. In Advances in Neural Information Processing Systems. 6367\u20136377."},{"key":"e_1_3_3_37_2","first-page":"389","volume-title":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","author":"Yang Pengfei","year":"2021","unstructured":"Pengfei Yang, Renjue Li, Jianlin Li, Cheng-Chao Huang, Jingyi Wang, Jun Sun, Bai Xue, and Lijun Zhang. 2021. Improving neural network verification through spurious region guided refinement. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 389\u2013408."}],"container-title":["ACM Transactions on Design Automation of Electronic Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3611671","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3611671","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:37:08Z","timestamp":1750178228000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3611671"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,10,16]]},"references-count":36,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2023,11,30]]}},"alternative-id":["10.1145\/3611671"],"URL":"https:\/\/doi.org\/10.1145\/3611671","relation":{},"ISSN":["1084-4309","1557-7309"],"issn-type":[{"type":"print","value":"1084-4309"},{"type":"electronic","value":"1557-7309"}],"subject":[],"published":{"date-parts":[[2023,10,16]]},"assertion":[{"value":"2022-11-28","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-07-24","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-10-16","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}