{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T20:16:24Z","timestamp":1784837784102,"version":"3.55.0"},"reference-count":33,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,1,2]],"date-time":"2019-01-02T00:00:00Z","timestamp":1546387200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-sa\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100001711","name":"Schweizerischer Nationalfonds zur F\u00f6rderung der Wissenschaftlichen Forschung","doi-asserted-by":"publisher","award":["163117"],"award-info":[{"award-number":["163117"]}],"id":[{"id":"10.13039\/501100001711","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2019,1,2]]},"abstract":"<jats:p>We present a novel method for scalable and precise certification of deep neural networks. The key technical insight behind our approach is a new abstract domain which combines floating point polyhedra with intervals and is equipped with abstract transformers specifically tailored to the setting of neural networks. Concretely, we introduce new transformers for affine transforms, the rectified linear unit (ReLU), sigmoid, tanh, and maxpool functions.<\/jats:p>\n          <jats:p>We implemented our method in a system called DeepPoly and evaluated it extensively on a range of datasets, neural architectures (including defended networks), and specifications. Our experimental results indicate that DeepPoly is more precise than prior work while scaling to large networks.<\/jats:p>\n          <jats:p>We also show how to combine DeepPoly with a form of abstraction refinement based on trace partitioning. This enables us to prove, for the first time, the robustness of the network when the input image is subjected to complex perturbations such as rotations that employ linear interpolation.<\/jats:p>","DOI":"10.1145\/3290354","type":"journal-article","created":{"date-parts":[[2019,1,4]],"date-time":"2019-01-04T13:33:51Z","timestamp":1546608831000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":454,"title":["An abstract domain for certifying neural networks"],"prefix":"10.1145","volume":"3","author":[{"given":"Gagandeep","family":"Singh","sequence":"first","affiliation":[{"name":"ETH Zurich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Timon","family":"Gehr","sequence":"additional","affiliation":[{"name":"ETH Zurich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Markus","family":"P\u00fcschel","sequence":"additional","affiliation":[{"name":"ETH Zurich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Martin","family":"Vechev","sequence":"additional","affiliation":[{"name":"ETH Zurich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,1,2]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.2478\/v10136-012-0031-x"},{"key":"e_1_2_2_2_1","volume-title":"Proc. Neural Information Processing Systems (NIPS). 2621\u20132629","author":"Bastani Osbert","year":"2016","unstructured":"Osbert Bastani , Yani Ioannou , Leonidas Lampropoulos , Dimitrios Vytiniotis , Aditya V. Nori , and Antonio Criminisi . 2016 . Measuring Neural Net Robustness with Constraints . In Proc. Neural Information Processing Systems (NIPS). 2621\u20132629 . Osbert Bastani, Yani Ioannou, Leonidas Lampropoulos, Dimitrios Vytiniotis, Aditya V. Nori, and Antonio Criminisi. 2016. Measuring Neural Net Robustness with Constraints. In Proc. Neural Information Processing Systems (NIPS). 2621\u20132629."},{"key":"e_1_2_2_3_1","volume-title":"Davide Del Testa","author":"Bojarski Mariusz","year":"2016","unstructured":"Mariusz Bojarski , Davide Del Testa , Daniel Dworakowski, Bernhard Firner , Beat Flepp, Prasoon Goyal, Lawrence D. Jackel, Mathew Monfort, Urs Muller, Jiakai Zhang, Xin Zhang, Jake Zhao, and Karol Zieba. 2016 . End to End Learning for Self-Driving Cars. CoRR abs\/1604.07316 (2016). Mariusz Bojarski, Davide Del Testa, Daniel Dworakowski, Bernhard Firner, Beat Flepp, Prasoon Goyal, Lawrence D. Jackel, Mathew Monfort, Urs Muller, Jiakai Zhang, Xin Zhang, Jake Zhao, and Karol Zieba. 2016. End to End Learning for Self-Driving Cars. CoRR abs\/1604.07316 (2016)."},{"key":"e_1_2_2_4_1","volume-title":"Dill","author":"Carlini Nicholas","year":"2017","unstructured":"Nicholas Carlini , Guy Katz , Clark Barrett , and David L . Dill . 2017 . Ground-Truth Adversarial Examples. CoRR abs\/1709.10207 (2017). Nicholas Carlini, Guy Katz, Clark Barrett, and David L. Dill. 2017. Ground-Truth Adversarial Examples. CoRR abs\/1709.10207 (2017)."},{"key":"e_1_2_2_5_1","volume-title":"Proc. IEEE Symposium on Security and Privacy (SP). 39\u201357","author":"Carlini Nicholas","unstructured":"Nicholas Carlini and David A. Wagner . 2017. Towards Evaluating the Robustness of Neural Networks . In Proc. IEEE Symposium on Security and Privacy (SP). 39\u201357 . Nicholas Carlini and David A. Wagner. 2017. Towards Evaluating the Robustness of Neural Networks. In Proc. IEEE Symposium on Security and Privacy (SP). 39\u201357."},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/512760.512770"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/CVPR.2018.00957"},{"key":"e_1_2_2_8_1","volume-title":"Proc. Uncertainty in Artificial Intelligence (UAI). 162\u2013171","author":"Dvijotham Krishnamurthy","year":"2018","unstructured":"Krishnamurthy Dvijotham , Robert Stanforth , Sven Gowal , Timothy Mann , and Pushmeet Kohli . 2018 . A Dual Approach to Scalable Verification of Deep Networks . In Proc. Uncertainty in Artificial Intelligence (UAI). 162\u2013171 . Krishnamurthy Dvijotham, Robert Stanforth, Sven Gowal, Timothy Mann, and Pushmeet Kohli. 2018. A Dual Approach to Scalable Verification of Deep Networks. In Proc. Uncertainty in Artificial Intelligence (UAI). 162\u2013171."},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-68167-2_19"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2018.00058"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_47"},{"key":"e_1_2_2_12_1","volume-title":"Proc. International Conference on Learning Representations (ICLR).","author":"Goodfellow Ian","year":"2015","unstructured":"Ian Goodfellow , Jonathon Shlens , and Christian Szegedy . 2015 . Explaining and Harnessing Adversarial Examples . In Proc. International Conference on Learning Representations (ICLR). Ian Goodfellow, Jonathon Shlens, and Christian Szegedy. 2015. Explaining and Harnessing Adversarial Examples. In Proc. International Conference on Learning Representations (ICLR)."},{"key":"e_1_2_2_13_1","volume-title":"McDaniel","author":"Grosse Kathrin","year":"2016","unstructured":"Kathrin Grosse , Nicolas Papernot , Praveen Manoharan , Michael Backes , and Patrick D . McDaniel . 2016 . Adversarial Perturbations Against Deep Neural Networks for Malware Classification. CoRR abs\/1606.04435 (2016). http:\/\/arxiv.org\/ abs\/1606.04435 Kathrin Grosse, Nicolas Papernot, Praveen Manoharan, Michael Backes, and Patrick D. McDaniel. 2016. Adversarial Perturbations Against Deep Neural Networks for Malware Classification. CoRR abs\/1606.04435 (2016). http:\/\/arxiv.org\/ abs\/1606.04435"},{"key":"e_1_2_2_14_1","volume-title":"Towards deep neural network architectures robust to adversarial examples. arXiv preprint arXiv:1412.5068","author":"Gu Shixiang","year":"2014","unstructured":"Shixiang Gu and Luca Rigazio . 2014. Towards deep neural network architectures robust to adversarial examples. arXiv preprint arXiv:1412.5068 ( 2014 ). Shixiang Gu and Luca Rigazio. 2014. Towards deep neural network architectures robust to adversarial examples. arXiv preprint arXiv:1412.5068 (2014)."},{"key":"e_1_2_2_15_1","volume-title":"Proc. International Conference on Computer Aided Verification (CAV). 97\u2013117","author":"Katz Guy","unstructured":"Guy Katz , Clark W. Barrett , David L. Dill , Kyle Julian , and Mykel J. Kochenderfer . 2017. Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks . In Proc. International Conference on Computer Aided Verification (CAV). 97\u2013117 . Guy Katz, Clark W. Barrett, David L. Dill, Kyle Julian, and Mykel J. Kochenderfer. 2017. Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. In Proc. International Conference on Computer Aided Verification (CAV). 97\u2013117."},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/5.726791"},{"key":"e_1_2_2_18_1","volume-title":"Proc. International Conference on Learning Representations (ICLR).","author":"Madry Aleksander","year":"2018","unstructured":"Aleksander Madry , Aleksandar Makelov , Ludwig Schmidt , Dimitris Tsipras , and Adrian Vladu . 2018 . Towards deep learning models resistant to adversarial attacks . In Proc. International Conference on Learning Representations (ICLR). Aleksander Madry, Aleksandar Makelov, Ludwig Schmidt, Dimitris Tsipras, and Adrian Vladu. 2018. Towards deep learning models resistant to adversarial attacks. In Proc. International Conference on Learning Representations (ICLR)."},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24725-8_2"},{"key":"e_1_2_2_20_1","volume-title":"Proc. International Conference on Machine Learning (ICML). 3575\u20133583","author":"Mirman Matthew","year":"2018","unstructured":"Matthew Mirman , Timon Gehr , and Martin Vechev . 2018 . Differentiable Abstract Interpretation for Provably Robust Neural Networks . In Proc. International Conference on Machine Learning (ICML). 3575\u20133583 . Matthew Mirman, Timon Gehr, and Martin Vechev. 2018. Differentiable Abstract Interpretation for Provably Robust Neural Networks. In Proc. International Conference on Machine Learning (ICML). 3575\u20133583."},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/CVPR.2015.7298640"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132785"},{"key":"e_1_2_2_23_1","volume-title":"Towards Practical Verification of Machine Learning: The Case of Computer Vision Systems. CoRR abs\/1712.01785","author":"Pei Kexin","year":"2017","unstructured":"Kexin Pei , Yinzhi Cao , Junfeng Yang , and Suman Jana . 2017b. Towards Practical Verification of Machine Learning: The Case of Computer Vision Systems. CoRR abs\/1712.01785 ( 2017 ). Kexin Pei, Yinzhi Cao, Junfeng Yang, and Suman Jana. 2017b. Towards Practical Verification of Machine Learning: The Case of Computer Vision Systems. CoRR abs\/1712.01785 (2017)."},{"key":"e_1_2_2_24_1","volume-title":"Proc. International Conference on Machine Learning (ICML).","author":"Raghunathan Aditi","year":"2018","unstructured":"Aditi Raghunathan , Jacob Steinhardt , and Percy Liang . 2018 . Certified Defenses against Adversarial Examples . In Proc. International Conference on Machine Learning (ICML). Aditi Raghunathan, Jacob Steinhardt, and Percy Liang. 2018. Certified Defenses against Adversarial Examples. In Proc. International Conference on Machine Learning (ICML)."},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1275497.1275501"},{"key":"e_1_2_2_26_1","volume-title":"Fleet","author":"Sabour Sara","year":"2015","unstructured":"Sara Sabour , Yanshuai Cao , Fartash Faghri , and David J . Fleet . 2015 . Adversarial Manipulation of Deep Representations. CoRR abs\/1511.05122 (2015). Sara Sabour, Yanshuai Cao, Fartash Faghri, and David J. Fleet. 2015. Adversarial Manipulation of Deep Representations. CoRR abs\/1511.05122 (2015)."},{"key":"e_1_2_2_27_1","volume-title":"Proc. Neural Information Processing Systems (NIPS).","author":"Singh Gagandeep","year":"2018","unstructured":"Gagandeep Singh , Timon Gehr , Matthew Mirman , Markus P\u00fcschel , and Martin Vechev . 2018 a. Fast and Effective Robustness Certification . In Proc. Neural Information Processing Systems (NIPS). Gagandeep Singh, Timon Gehr, Matthew Mirman, Markus P\u00fcschel, and Martin Vechev. 2018a. Fast and Effective Robustness Certification. In Proc. Neural Information Processing Systems (NIPS)."},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009885"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158143"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/IJCNN.2016.7727230"},{"key":"e_1_2_2_31_1","volume-title":"Verifying Neural Networks with Mixed Integer Programming. CoRR abs\/1711.07356","author":"Tjeng Vincent","year":"2017","unstructured":"Vincent Tjeng and Russ Tedrake . 2017. Verifying Neural Networks with Mixed Integer Programming. CoRR abs\/1711.07356 ( 2017 ). Vincent Tjeng and Russ Tedrake. 2017. Verifying Neural Networks with Mixed Integer Programming. CoRR abs\/1711.07356 (2017)."},{"key":"e_1_2_2_32_1","volume-title":"Proc. USENIX Security Symposium (USENIX Security 18)","author":"Wang Shiqi","year":"2018","unstructured":"Shiqi Wang , Kexin Pei , Justin Whitehouse , Junfeng Yang , and Suman Jana . 2018 . Formal Security Analysis of Neural Networks using Symbolic Intervals . In Proc. USENIX Security Symposium (USENIX Security 18) . 1599\u20131614. Shiqi Wang, Kexin Pei, Justin Whitehouse, Junfeng Yang, and Suman Jana. 2018. Formal Security Analysis of Neural Networks using Symbolic Intervals. In Proc. USENIX Security Symposium (USENIX Security 18). 1599\u20131614."},{"key":"e_1_2_2_33_1","volume-title":"Proc. International Conference on Machine Learning (ICML). 5273\u20135282","author":"Weng Tsui-Wei","year":"2018","unstructured":"Tsui-Wei Weng , Huan Zhang , Hongge Chen , Zhao Song , Cho-Jui Hsieh , Luca Daniel , Duane Boning , and Inderjit Dhillon . 2018 . Towards Fast Computation of Certified Robustness for ReLU Networks . In Proc. International Conference on Machine Learning (ICML). 5273\u20135282 . Tsui-Wei Weng, Huan Zhang, Hongge Chen, Zhao Song, Cho-Jui Hsieh, Luca Daniel, Duane Boning, and Inderjit Dhillon. 2018. Towards Fast Computation of Certified Robustness for ReLU Networks. In Proc. International Conference on Machine Learning (ICML). 5273\u20135282."},{"key":"e_1_2_2_34_1","volume-title":"Proc. International Conference on Machine Learning (ICML). 5283\u20135292","author":"Wong Eric","year":"2018","unstructured":"Eric Wong and Zico Kolter . 2018 . Provable Defenses against Adversarial Examples via the Convex Outer Adversarial Polytope . In Proc. International Conference on Machine Learning (ICML). 5283\u20135292 . Eric Wong and Zico Kolter. 2018. Provable Defenses against Adversarial Examples via the Convex Outer Adversarial Polytope. In Proc. International Conference on Machine Learning (ICML). 5283\u20135292."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290354","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3290354","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:58:04Z","timestamp":1750208284000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290354"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,2]]},"references-count":33,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2019,1,2]]}},"alternative-id":["10.1145\/3290354"],"URL":"https:\/\/doi.org\/10.1145\/3290354","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,1,2]]},"assertion":[{"value":"2019-01-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}