{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T20:54:31Z","timestamp":1760043271575,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":30,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,11,8]],"date-time":"2020-11-08T00:00:00Z","timestamp":1604793600000},"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":[[2020,11,8]]},"DOI":"10.1145\/3368089.3417918","type":"proceedings-article","created":{"date-parts":[[2020,11,8]],"date-time":"2020-11-08T06:03:52Z","timestamp":1604815432000},"page":"1630-1634","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":16,"title":["PRODeep: a platform for robustness verification of deep neural networks"],"prefix":"10.1145","author":[{"given":"Renjue","family":"Li","sequence":"first","affiliation":[{"name":"Institute of Software at Chinese Academy of Sciences, China \/ University of Chinese Academy of Sciences, China"}]},{"given":"Jianlin","family":"Li","sequence":"additional","affiliation":[{"name":"Institute of Software at Chinese Academy of Sciences, China \/ University of Chinese Academy of Sciences, China"}]},{"given":"Cheng-Chao","family":"Huang","sequence":"additional","affiliation":[{"name":"Institute of Intelligent Software, China"}]},{"given":"Pengfei","family":"Yang","sequence":"additional","affiliation":[{"name":"Institute of Software at Chinese Academy of Sciences, China \/ University of Chinese Academy of Sciences, China"}]},{"given":"Xiaowei","family":"Huang","sequence":"additional","affiliation":[{"name":"University of Liverpool, UK"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3692-2088","authenticated-orcid":false,"given":"Lijun","family":"Zhang","sequence":"additional","affiliation":[{"name":"Institute of Software at Chinese Academy of Sciences, China"}]},{"given":"Bai","family":"Xue","sequence":"additional","affiliation":[{"name":"Institute of Software at Chinese Academy of Sciences, China"}]},{"given":"Holger","family":"Hermanns","sequence":"additional","affiliation":[{"name":"Saarland University, Germany"}]}],"member":"320","published-online":{"date-parts":[[2020,11,8]]},"reference":[{"key":"e_1_3_2_2_1_1","unstructured":"Abadi M. Agarwal A. Barham P. Brevdo E. Chen Z. Citro C. Corrado G. S. Davis A. Dean J. Devin M. Ghemawat S. Goodfellow I. Harp A. Irving G. Isard M. Jia Y. Jozefowicz R. Kaiser L. Kudlur M. Levenberg J. Man\u00e9 D. Monga R. Moore S. Murray D. Olah C. Schuster M. Shlens J. Steiner B. Sutskever I. Talwar K. Tucker P. Vanhoucke V. Vasudevan V. Vi\u00e9gas F. Vinyals O. Warden P. Wattenberg M. Wicke M. Yu Y. and Zheng X. TensorFlow: Large-scale machine learning on heterogeneous systems 2015. Software available from tensorflow. org.  Abadi M. Agarwal A. Barham P. Brevdo E. Chen Z. Citro C. Corrado G. S. Davis A. Dean J. Devin M. Ghemawat S. Goodfellow I. Harp A. Irving G. Isard M. Jia Y. Jozefowicz R. Kaiser L. Kudlur M. Levenberg J. Man\u00e9 D. Monga R. Moore S. Murray D. Olah C. Schuster M. Shlens J. Steiner B. Sutskever I. Talwar K. Tucker P. Vanhoucke V. Vasudevan V. Vi\u00e9gas F. Vinyals O. Warden P. Wattenberg M. Wicke M. Yu Y. and Zheng X. TensorFlow: Large-scale machine learning on heterogeneous systems 2015. Software available from tensorflow. org."},{"key":"e_1_3_2_2_2_1","first-page":"184","volume-title":"Principles of Knowledge Representation and Reasoning: Proceedings of the Sixteenth International Conference, KR 2018","author":"Akintunde M.","year":"2018","unstructured":"Akintunde , M. , Lomuscio , A. , Maganti , L. , and Pirovano , E . Reachability analysis for neural agent-environment systems . In Principles of Knowledge Representation and Reasoning: Proceedings of the Sixteenth International Conference, KR 2018 , Tempe, Arizona , 30 October -2 November 2018 ( 2018 ), M. Thielscher, F. Toni, and F. Wolter, Eds., AAAI Press, pp. 184 - 193 . Akintunde, M., Lomuscio, A., Maganti, L., and Pirovano, E. Reachability analysis for neural agent-environment systems. In Principles of Knowledge Representation and Reasoning: Proceedings of the Sixteenth International Conference, KR 2018, Tempe, Arizona, 30 October-2 November 2018 ( 2018 ), M. Thielscher, F. Toni, and F. Wolter, Eds., AAAI Press, pp. 184-193."},{"key":"e_1_3_2_2_3_1","volume-title":"Optimization and Abstraction: A Synergistic Approach for Analyzing Neural Network Robustness. arXiv e-prints (Apr. 2019 ), arXiv","author":"Anderson G.","year":"1904","unstructured":"Anderson , G. , Pailoor , S. , Dillig , I. , and Chaudhuri , S . Optimization and Abstraction: A Synergistic Approach for Analyzing Neural Network Robustness. arXiv e-prints (Apr. 2019 ), arXiv : 1904 .09959. Anderson, G., Pailoor, S., Dillig, I., and Chaudhuri, S. Optimization and Abstraction: A Synergistic Approach for Analyzing Neural Network Robustness. arXiv e-prints (Apr. 2019 ), arXiv: 1904.09959."},{"key":"e_1_3_2_2_4_1","first-page":"15287","volume-title":"Advances in Neural Information Processing Systems 32: Annual Conference on Neural Information Processing Systems 2019","author":"Balunovic M.","year":"2019","unstructured":"Balunovic , M. , Baader , M. , Singh , G. , Gehr , T. , and Vechev , M. T . Certifying geometric robustness of neural networks . In Advances in Neural Information Processing Systems 32: Annual Conference on Neural Information Processing Systems 2019 , NeurIPS 2019 , 8-14 December 2019, Vancouver, BC, Canada ( 2019 ), H. M. Wallach, H. Larochelle, A. Beygelzimer, F. d'Alch\u00e9-Buc, E. B. Fox, and R. Garnett, Eds., pp. 15287 - 15297 . Balunovic, M., Baader, M., Singh, G., Gehr, T., and Vechev, M. T. Certifying geometric robustness of neural networks. In Advances in Neural Information Processing Systems 32: Annual Conference on Neural Information Processing Systems 2019, NeurIPS 2019, 8-14 December 2019, Vancouver, BC, Canada ( 2019 ), H. M. Wallach, H. Larochelle, A. Beygelzimer, F. d'Alch\u00e9-Buc, E. B. Fox, and R. Garnett, Eds., pp. 15287-15297."},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v34i04.5729"},{"key":"e_1_3_2_2_6_1","first-page":"238","volume-title":"Fourth ACM Symposium on Principles of Programming Languages (POPL) ( 1977 )","author":"Cousot P.","unstructured":"Cousot , P. , and Cousot , R . Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints . In Fourth ACM Symposium on Principles of Programming Languages (POPL) ( 1977 ) , pp. 238 - 252 . Cousot, P., and Cousot, R. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Fourth ACM Symposium on Principles of Programming Languages (POPL) ( 1977 ), pp. 238-252."},{"key":"e_1_3_2_2_7_1","first-page":"121","volume-title":"NASA Formal Methods-10th International Symposium, NFM 2018, Newport News, VA, USA, April 17-19, 2018, Proceedings ( 2018 )","author":"Dutta S.","unstructured":"Dutta , S. , Jha , S. , Sankaranarayanan , S. , and Tiwari , A . Output range analysis for deep feedforward neural networks . In NASA Formal Methods-10th International Symposium, NFM 2018, Newport News, VA, USA, April 17-19, 2018, Proceedings ( 2018 ) , pp. 121 - 138 . Dutta, S., Jha, S., Sankaranarayanan, S., and Tiwari, A. Output range analysis for deep feedforward neural networks. In NASA Formal Methods-10th International Symposium, NFM 2018, Newport News, VA, USA, April 17-19, 2018, Proceedings ( 2018 ), pp. 121-138."},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-68167-2_19"},{"key":"e_1_3_2_2_9_1","first-page":"948","volume-title":"2018 IEEE Symposium on Security and Privacy (S&P 2018 ) ( 2018 )","author":"Gehr T.","unstructured":"Gehr , T. , Mirman , M. , Drachsler-Cohen , D. , Tsankov , P. , Chaudhuri , S. , and Vechev , M . AI2: Safety and robustness certification of neural networks with abstract interpretation . In 2018 IEEE Symposium on Security and Privacy (S&P 2018 ) ( 2018 ) , pp. 948 - 963 . Gehr, T., Mirman, M., Drachsler-Cohen, D., Tsankov, P., Chaudhuri, S., and Vechev, M. AI2: Safety and robustness certification of neural networks with abstract interpretation. In 2018 IEEE Symposium on Security and Privacy (S&P 2018 ) ( 2018 ), pp. 948-963."},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"crossref","unstructured":"Huang X. Kroening D. Ruan W. Sharp J. Sun Y. Thamo E. Wu M. and Yi X. A survey of safety and trustworthiness of deep neural networks: Verification testing adversarial attack and defence and interpretability. Computer Science Review ( 2020 ).  Huang X. Kroening D. Ruan W. Sharp J. Sun Y. Thamo E. Wu M. and Yi X. A survey of safety and trustworthiness of deep neural networks: Verification testing adversarial attack and defence and interpretability. Computer Science Review ( 2020 ).","DOI":"10.1016\/j.cosrev.2020.100270"},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63387-9_1"},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"crossref","unstructured":"Jia Y. Shelhamer E. Donahue J. Karayev S. Long J. Girshick R. Guadarrama S. and Darrell T. Cafe: Convolutional architecture for fast feature embedding. arXiv preprint arXiv:1408.5093 ( 2014 ).  Jia Y. Shelhamer E. Donahue J. Karayev S. Long J. Girshick R. Guadarrama S. and Darrell T. Cafe: Convolutional architecture for fast feature embedding. arXiv preprint arXiv:1408.5093 ( 2014 ).","DOI":"10.1145\/2647868.2654889"},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63387-9_5"},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_26"},{"key":"e_1_3_2_2_15_1","volume-title":"POPQORN: Quantifying Robustness of Recurrent Neural Networks. arXiv e-prints (May 2019 ), arXiv","author":"Ko C.-Y.","year":"1905","unstructured":"Ko , C.-Y. , Lyu , Z. , Weng , T.-W. , Daniel , L. , Wong , N. , and Lin , D . POPQORN: Quantifying Robustness of Recurrent Neural Networks. arXiv e-prints (May 2019 ), arXiv : 1905 .07387. Ko, C.-Y., Lyu, Z., Weng, T.-W., Daniel, L., Wong, N., and Lin, D. POPQORN: Quantifying Robustness of Recurrent Neural Networks. arXiv e-prints (May 2019 ), arXiv: 1905.07387."},{"key":"e_1_3_2_2_16_1","unstructured":"Krizhevsky A. Hinton G. etal Learning multiple layers of features from tiny images.  Krizhevsky A. Hinton G. et al. Learning multiple layers of features from tiny images."},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/5.726791"},{"key":"e_1_3_2_2_18_1","first-page":"296","volume-title":"Static Analysis-26th International Symposium, SAS 2019, Porto, Portugal, October 8-11, 2019, Proceedings ( 2019 ), B. E. Chang, Ed.","volume":"11822","author":"Li J.","unstructured":"Li , J. , Liu , J. , Yang , P. , Chen , L. , Huang , X. , and Zhang , L . Analyzing deep neural networks with symbolic propagation: Towards higher precision and faster verification . In Static Analysis-26th International Symposium, SAS 2019, Porto, Portugal, October 8-11, 2019, Proceedings ( 2019 ), B. E. Chang, Ed. , vol. 11822 of Lecture Notes in Computer Science, Springer , pp. 296 - 319 . Li, J., Liu, J., Yang, P., Chen, L., Huang, X., and Zhang, L. Analyzing deep neural networks with symbolic propagation: Towards higher precision and faster verification. In Static Analysis-26th International Symposium, SAS 2019, Porto, Portugal, October 8-11, 2019, Proceedings ( 2019 ), B. E. Chang, Ed., vol. 11822 of Lecture Notes in Computer Science, Springer, pp. 296-319."},{"key":"e_1_3_2_2_19_1","first-page":"8024","volume-title":"Advances in Neural Information Processing Systems 32, H. Wallach, H. Larochelle, A. Beygelzimer, F. d'Alch\u00e9-Buc","author":"Paszke A.","year":"2019","unstructured":"Paszke , A. , Gross , S. , Massa , F. , Lerer , A. , Bradbury , J. , Chanan , G. , Killeen , T. , Lin , Z. , Gimelshein , N. , Antiga , L. , Desmaison , A. , Kopf , A. , Yang , E. , DeVito , Z. , Raison , M. , Tejani , A. , Chilamkurthy , S. , Steiner , B. , Fang , L. , Bai , J. , and Chintala , S . Pytorch: An imperative style, high-performance deep learning library . In Advances in Neural Information Processing Systems 32, H. Wallach, H. Larochelle, A. Beygelzimer, F. d'Alch\u00e9-Buc , E. Fox, and R. Garnett, Eds. Curran Associates, Inc. , 2019 , pp. 8024 - 8035 . Paszke, A., Gross, S., Massa, F., Lerer, A., Bradbury, J., Chanan, G., Killeen, T., Lin, Z., Gimelshein, N., Antiga, L., Desmaison, A., Kopf, A., Yang, E., DeVito, Z., Raison, M., Tejani, A., Chilamkurthy, S., Steiner, B., Fang, L., Bai, J., and Chintala, S. Pytorch: An imperative style, high-performance deep learning library. In Advances in Neural Information Processing Systems 32, H. Wallach, H. Larochelle, A. Beygelzimer, F. d'Alch\u00e9-Buc, E. Fox, and R. Garnett, Eds. Curran Associates, Inc., 2019, pp. 8024-8035."},{"key":"e_1_3_2_2_20_1","first-page":"243","volume-title":"22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010. Proceedings ( 2010 )","author":"Pulina L.","unstructured":"Pulina , L. , and Tacchella , A . An abstraction-refinement approach to verification of artificial neural networks. In Computer Aided Verification , 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010. Proceedings ( 2010 ) , pp. 243 - 257 . Pulina, L., and Tacchella, A. An abstraction-refinement approach to verification of artificial neural networks. In Computer Aided Verification, 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010. Proceedings ( 2010 ), pp. 243-257."},{"key":"e_1_3_2_2_21_1","first-page":"2651","volume-title":"IJCAI2018 ( 2018 )","author":"Ruan W.","unstructured":"Ruan , W. , Huang , X. , and Kwiatkowska , M . Reachability analysis of deep neural networks with provable guarantees . In IJCAI2018 ( 2018 ) , pp. 2651 - 2659 . Ruan, W., Huang, X., and Kwiatkowska, M. Reachability analysis of deep neural networks with provable guarantees. In IJCAI2018 ( 2018 ), pp. 2651-2659."},{"key":"e_1_3_2_2_22_1","first-page":"10825","volume-title":"Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018","author":"Singh G.","year":"2018","unstructured":"Singh , G. , Gehr , T. , Mirman , M. , P\u00fcschel , M. , and Vechev , M. T . Fast and efective robustness certification . In Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018 , NeurIPS 2018 , 3-8 December 2018, Montr\u00e9al, Canada. ( 2018 ), pp. 10825 - 10836 . Singh, G., Gehr, T., Mirman, M., P\u00fcschel, M., and Vechev, M. T. Fast and efective robustness certification. In Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018, NeurIPS 2018, 3-8 December 2018, Montr\u00e9al, Canada. ( 2018 ), pp. 10825-10836."},{"volume-title":"Proc. ACM Program. Lang. 3, POPL ( 2019 ), 41 : 1-41 : 30","author":"Singh G.","key":"e_1_3_2_2_23_1","unstructured":"Singh , G. , Gehr , T. , P\u00fcschel , M. , and Vechev , M. T . An abstract domain for certifying neural networks . Proc. ACM Program. Lang. 3, POPL ( 2019 ), 41 : 1-41 : 30 . Singh, G., Gehr, T., P\u00fcschel, M., and Vechev, M. T. An abstract domain for certifying neural networks. Proc. ACM Program. Lang. 3, POPL ( 2019 ), 41 : 1-41 : 30."},{"key":"e_1_3_2_2_24_1","doi-asserted-by":"crossref","unstructured":"Singh G. Gehr T. P\u00fcschel M. and Vechev M. T. An abstract domain for certifying neural networks. PACMPL 3 POPL ( 2019 ) 41 : 1-41 : 30.  Singh G. Gehr T. P\u00fcschel M. and Vechev M. T. An abstract domain for certifying neural networks. PACMPL 3 POPL ( 2019 ) 41 : 1-41 : 30.","DOI":"10.1145\/3290354"},{"volume-title":"33rd IEEE\/ACM International Conference on ( 2018 ).","author":"Sun Y.","key":"e_1_3_2_2_25_1","unstructured":"Sun , Y. , Wu , M. , Ruan , W. , Huang , X. , Kwiatkowska , M. , and Kroening , D . Concolic testing for deep neural networks. In Automated Software Engineering (ASE) , 33rd IEEE\/ACM International Conference on ( 2018 ). Sun, Y., Wu, M., Ruan, W., Huang, X., Kwiatkowska, M., and Kroening, D. Concolic testing for deep neural networks. In Automated Software Engineering (ASE), 33rd IEEE\/ACM International Conference on ( 2018 )."},{"key":"e_1_3_2_2_26_1","first-page":"1245","volume-title":"2019 IEEE\/ACM 41st International Conference on Software Engineering (ICSE) ( 2019 )","author":"Wang J.","unstructured":"Wang , J. , Dong , G. , Sun , J. , Wang , X. , and Zhang , P . Adversarial sample detection for deep neural network through model mutation testing . In 2019 IEEE\/ACM 41st International Conference on Software Engineering (ICSE) ( 2019 ) , pp. 1245 - 1256 . Wang, J., Dong, G., Sun, J., Wang, X., and Zhang, P. Adversarial sample detection for deep neural network through model mutation testing. In 2019 IEEE\/ACM 41st International Conference on Software Engineering (ICSE) ( 2019 ), pp. 1245-1256."},{"key":"e_1_3_2_2_27_1","volume-title":"Towards Fast Computation of Certified Robustness for ReLU Networks. arXiv e-prints (Apr. 2018 ), arXiv","author":"Weng T.-W.","year":"1804","unstructured":"Weng , T.-W. , Zhang , H. , Chen , H. , Song , Z. , Hsieh , C.-J. , Boning , D. , Dhillon , I. S. , and Daniel , L . Towards Fast Computation of Certified Robustness for ReLU Networks. arXiv e-prints (Apr. 2018 ), arXiv : 1804 .09699. Weng, T.-W., Zhang, H., Chen, H., Song, Z., Hsieh, C.-J., Boning, D., Dhillon, I. S., and Daniel, L. Towards Fast Computation of Certified Robustness for ReLU Networks. arXiv e-prints (Apr. 2018 ), arXiv: 1804.09699."},{"key":"e_1_3_2_2_28_1","volume-title":"Evaluating the Robustness of Neural Networks: An Extreme Value Theory Approach. arXiv e-prints (Jan. 2018 ), arXiv","author":"Weng T.-W.","year":"1801","unstructured":"Weng , T.-W. , Zhang , H. , Chen , P.-Y. , Yi , J. , Su , D. , Gao , Y. , Hsieh , C.-J. , and Daniel , L . Evaluating the Robustness of Neural Networks: An Extreme Value Theory Approach. arXiv e-prints (Jan. 2018 ), arXiv : 1801 .10578. Weng, T.-W., Zhang, H., Chen, P.-Y., Yi, J., Su, D., Gao, Y., Hsieh, C.-J., and Daniel, L. Evaluating the Robustness of Neural Networks: An Extreme Value Theory Approach. arXiv e-prints (Jan. 2018 ), arXiv: 1801.10578."},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89960-2_22"},{"key":"e_1_3_2_2_30_1","doi-asserted-by":"crossref","unstructured":"Wu M. Wicker M. Ruan W. Huang X. and Kwiatkowska M. A gamebased approximate verification of deep neural networks with provable guarantees. Theoretical Computer Science 807 ( 2020 ) 298-329.  Wu M. Wicker M. Ruan W. Huang X. and Kwiatkowska M. A gamebased approximate verification of deep neural networks with provable guarantees. Theoretical Computer Science 807 ( 2020 ) 298-329.","DOI":"10.1016\/j.tcs.2019.05.046"}],"event":{"name":"ESEC\/FSE '20: 28th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering"],"location":"Virtual Event USA","acronym":"ESEC\/FSE '20"},"container-title":["Proceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3368089.3417918","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3368089.3417918","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:01:58Z","timestamp":1750197718000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3368089.3417918"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,11,8]]},"references-count":30,"alternative-id":["10.1145\/3368089.3417918","10.1145\/3368089"],"URL":"https:\/\/doi.org\/10.1145\/3368089.3417918","relation":{},"subject":[],"published":{"date-parts":[[2020,11,8]]},"assertion":[{"value":"2020-11-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}