{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T02:40:11Z","timestamp":1774838411480,"version":"3.50.1"},"reference-count":66,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2023,6,6]],"date-time":"2023-06-06T00:00:00Z","timestamp":1686009600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2023,6,6]]},"abstract":"<jats:p>We present a new abstract interpretation framework for the precise over-approximation of numerical fixpoint iterators.  \nOur key observation is that unlike in standard abstract interpretation (AI), typically used to over-approximate all reachable program states, in this setting, one only needs to abstract the concrete fixpoints, i.e., the final program states. Our framework targets numerical fixpoint iterators with convergence and uniqueness guarantees in the concrete and is based on two major technical contributions: (i) theoretical insights which allow us to compute sound and precise fixpoint abstractions without using joins, and (ii) a new abstract domain, CH-Zonotope, which admits efficient propagation and inclusion checks while retaining high precision.<\/jats:p>\n          <jats:p>We implement our framework in a tool called CRAFT and evaluate it on a novel fixpoint-based neural network architecture (monDEQ) that is particularly challenging to verify. Our extensive evaluation demonstrates that CRAFT exceeds the state-of-the-art performance in terms of speed (two orders of magnitude), scalability (one order of magnitude), and precision (25% higher certified accuracies).<\/jats:p>","DOI":"10.1145\/3591252","type":"journal-article","created":{"date-parts":[[2023,6,6]],"date-time":"2023-06-06T20:06:24Z","timestamp":1686081984000},"page":"786-810","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Abstract Interpretation of Fixpoint Iterators with Applications to Neural Networks"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2496-6542","authenticated-orcid":false,"given":"Mark Niklas","family":"M\u00fcller","sequence":"first","affiliation":[{"name":"ETH Zurich, Switzerland"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4157-1235","authenticated-orcid":false,"given":"Marc","family":"Fischer","sequence":"additional","affiliation":[{"name":"ETH Zurich, Switzerland"}]},{"ORCID":"https:\/\/orcid.org\/0009-0009-9040-1214","authenticated-orcid":false,"given":"Robin","family":"Staab","sequence":"additional","affiliation":[{"name":"ETH Zurich, Switzerland"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0054-9568","authenticated-orcid":false,"given":"Martin","family":"Vechev","sequence":"additional","affiliation":[{"name":"ETH Zurich, Switzerland"}]}],"member":"320","published-online":{"date-parts":[[2023,6,6]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.3182\/20080706-5-KR-1001.00861"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2012.09.003"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2015.12.005"},{"key":"e_1_2_1_4_1","volume":"201","author":"Amos Brandon","unstructured":"Brandon Amos and J. Zico Kolter. 201 7. OptNet: Differentiable Optimization as a Layer in Neural Networks. In Proc. of ICML. 70. Brandon Amos and J. Zico Kolter. 2017. OptNet: Differentiable Optimization as a Layer in Neural Networks. In Proc. of ICML. 70.","journal-title":"J. Zico Kolter."},{"key":"e_1_2_1_5_1","volume-title":"Proc. of NeurIPS.","author":"Bai Shaojie","year":"2019","unstructured":"Shaojie Bai , J. Zico Kolter , and Vladlen Koltun . 2019 . Deep Equilibrium Models . In Proc. of NeurIPS. Shaojie Bai, J. Zico Kolter, and Vladlen Koltun. 2019. Deep Equilibrium Models. In Proc. of NeurIPS."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36377-7_5"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0039704"},{"key":"e_1_2_1_8_1","unstructured":"Tong Chen Jean B. Lasserre Victor Magron and Edouard Pauwels. 2021. Semialgebraic Representation of Monotone Deep Equilibrium Models and Applications to Certification. \t\t\t\t  Tong Chen Jean B. Lasserre Victor Magron and Edouard Pauwels. 2021. Semialgebraic Representation of Monotone Deep Equilibrium Models and Applications to Certification."},{"key":"e_1_2_1_9_1","volume":"201","author":"Cohen Jeremy M.","unstructured":"Jeremy M. Cohen , Elan Rosenfeld , and J. Zico Kolter. 201 9. Certified Adversarial Robustness via Randomized Smoothing. In Proc. of ICML. 97. Jeremy M. Cohen, Elan Rosenfeld, and J. Zico Kolter. 2019. Certified Adversarial Robustness via Randomized Smoothing. In Proc. of ICML. 97.","journal-title":"J. Zico Kolter."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.23919\/ECC.2003.7085991"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_1_12_1","volume-title":"Formal Description of Programming Concepts: Proceedings of the IFIP Working Conference on Formal Description of Programming Concepts, St. Andrews","author":"Cousot Patrick","year":"1977","unstructured":"Patrick Cousot and Radhia Cousot . 1977. Static Determination of Dynamic Properties of Recursive Procedures . In Formal Description of Programming Concepts: Proceedings of the IFIP Working Conference on Formal Description of Programming Concepts, St. Andrews , NB , Canada, August 1-5, 1977 . Patrick Cousot and Radhia Cousot. 1977. Static Determination of Dynamic Properties of Recursive Procedures. In Formal Description of Programming Concepts: Proceedings of the IFIP Working Conference on Formal Description of Programming Concepts, St. Andrews, NB, Canada, August 1-5, 1977."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.2140\/pjm.1979.82.43"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/2.4.511"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-55844-6_142"},{"key":"e_1_2_1_16_1","volume-title":"Nikola Jovanovic, and Martin T. Vechev.","author":"Ferrari Claudio","year":"2022","unstructured":"Claudio Ferrari , Mark Niklas M\u00fcller , Nikola Jovanovic, and Martin T. Vechev. 2022 . Complete Verification via Multi-Neuron Relaxation Guided Branch-and-Bound. In Proc. of ICLR. Claudio Ferrari, Mark Niklas M\u00fcller, Nikola Jovanovic, and Martin T. Vechev. 2022. Complete Verification via Multi-Neuron Relaxation Guided Branch-and-Bound. In Proc. of ICLR."},{"key":"e_1_2_1_17_1","volume-title":"Proc. of ICLR.","author":"Fu Feisi","year":"2022","unstructured":"Feisi Fu and Wenchao Li . 2022 . Sound and Complete Neural Network Repair with Minimality and Locality Guarantees . In Proc. of ICLR. Feisi Fu and Wenchao Li. 2022. Sound and Complete Neural Network Repair with Minimality and Locality Guarantees. In Proc. of ICLR."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38856-9_3"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2018.00058"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1137\/20M1358517"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_47"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31954-2_19"},{"key":"e_1_2_1_23_1","volume-title":"Proc. of ICLR.","author":"Goodfellow Ian J.","year":"2015","unstructured":"Ian J. Goodfellow , Jonathon Shlens , and Christian Szegedy . 2015 . Explaining and Harnessing Adversarial Examples . In Proc. of ICLR. Ian J. Goodfellow, Jonathon Shlens, and Christian Szegedy. 2015. Explaining and Harnessing Adversarial Examples. In Proc. of ICLR."},{"key":"#cr-split#-e_1_2_1_24_1.1","unstructured":"Eric Goubault and Sylvie Putot. 2008. Perturbed affine arithmetic for invariant computation in numerical program analysis. CoRR https:\/\/doi.org\/10.48550\/arXiv.0807.2961 10.48550\/arXiv.0807.2961"},{"key":"#cr-split#-e_1_2_1_24_1.2","unstructured":"Eric Goubault and Sylvie Putot. 2008. Perturbed affine arithmetic for invariant computation in numerical program analysis. CoRR https:\/\/doi.org\/10.48550\/arXiv.0807.2961"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-79707-4_3"},{"key":"e_1_2_1_26_1","volume-title":"On the Effectiveness of Interval Bound Propagation for Training Verifiably Robust Models. ArXiv preprint, abs\/1810.12715","author":"Gowal Sven","year":"2018","unstructured":"Sven Gowal , Krishnamurthy Dvijotham , Robert Stanforth , Rudy Bunel , Chongli Qin , Jonathan Uesato , Relja Arandjelovic , Timothy A. Mann , and Pushmeet Kohli . 2018. On the Effectiveness of Interval Bound Propagation for Training Verifiably Robust Models. ArXiv preprint, abs\/1810.12715 ( 2018 ), https:\/\/doi.org\/10.48550\/arXiv.1810.12715 10.48550\/arXiv.1810.12715 Sven Gowal, Krishnamurthy Dvijotham, Robert Stanforth, Rudy Bunel, Chongli Qin, Jonathan Uesato, Relja Arandjelovic, Timothy A. Mann, and Pushmeet Kohli. 2018. On the Effectiveness of Interval Bound Propagation for Training Verifiably Robust Models. ArXiv preprint, abs\/1810.12715 (2018), https:\/\/doi.org\/10.48550\/arXiv.1810.12715"},{"key":"e_1_2_1_27_1","volume-title":"An Alternative Surrogate Loss for PGD-based Adversarial Testing. ArXiv preprint, abs\/1910.09338","author":"Gowal Sven","year":"2019","unstructured":"Sven Gowal , Jonathan Uesato , Chongli Qin , Po-Sen Huang , Timothy A. Mann , and Pushmeet Kohli . 2019. An Alternative Surrogate Loss for PGD-based Adversarial Testing. ArXiv preprint, abs\/1910.09338 ( 2019 ), https:\/\/doi.org\/10.48550\/arXiv.1910.09338 10.48550\/arXiv.1910.09338 Sven Gowal, Jonathan Uesato, Chongli Qin, Po-Sen Huang, Timothy A. Mann, and Pushmeet Kohli. 2019. An Alternative Surrogate Loss for PGD-based Adversarial Testing. ArXiv preprint, abs\/1910.09338 (2019), https:\/\/doi.org\/10.48550\/arXiv.1910.09338"},{"key":"e_1_2_1_28_1","unstructured":"Dwight Guth. 2013. A formal semantics of Python 3.3. \t\t\t\t  Dwight Guth. 2013. A formal semantics of Python 3.3."},{"key":"e_1_2_1_29_1","volume-title":"Faster Dynamic Matrix Inverse for Faster LPs. ArXiv preprint, abs\/2004.07470","author":"Jiang Shunhua","year":"2020","unstructured":"Shunhua Jiang , Zhao Song , Omri Weinstein , and Hengjie Zhang . 2020. Faster Dynamic Matrix Inverse for Faster LPs. ArXiv preprint, abs\/2004.07470 ( 2020 ), https:\/\/doi.org\/10.48550\/arXiv.2004.07470 10.48550\/arXiv.2004.07470 Shunhua Jiang, Zhao Song, Omri Weinstein, and Hengjie Zhang. 2020. Faster Dynamic Matrix Inverse for Faster LPs. ArXiv preprint, abs\/2004.07470 (2020), https:\/\/doi.org\/10.48550\/arXiv.2004.07470"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/DASC43569.2019.9081748"},{"key":"e_1_2_1_31_1","volume-title":"Containment problems for projections of polyhedra and spectrahedra. ArXiv preprint, abs\/1509.02735","author":"Kellner Kai","year":"2015","unstructured":"Kai Kellner . 2015. Containment problems for projections of polyhedra and spectrahedra. ArXiv preprint, abs\/1509.02735 ( 2015 ), https:\/\/doi.org\/10.48550\/arXiv.1509.02735 10.48550\/arXiv.1509.02735 Kai Kellner. 2015. Containment problems for projections of polyhedra and spectrahedra. ArXiv preprint, abs\/1509.02735 (2015), https:\/\/doi.org\/10.48550\/arXiv.1509.02735"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1063\/5.0060697"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2017.8264508"},{"key":"e_1_2_1_34_1","unstructured":"Alex Krizhevsky and Geoffrey Hinton. 2009. Learning multiple layers of features from tiny images. \t\t\t\t  Alex Krizhevsky and Geoffrey Hinton. 2009. Learning multiple layers of features from tiny images."},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF02684450"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ejcon.2021.06.028"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/5.726791"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2019.00044"},{"key":"e_1_2_1_39_1","volume-title":"Proc. of 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. of ICLR. Aleksander Madry, Aleksandar Makelov, Ludwig Schmidt, Dimitris Tsipras, and Adrian Vladu. 2018. Towards Deep Learning Models Resistant to Adversarial Attacks. In Proc. of ICLR."},{"key":"e_1_2_1_40_1","volume-title":"Vechev","author":"Mirman Matthew","year":"2018","unstructured":"Matthew Mirman , Timon Gehr , and Martin T . Vechev . 2018 . Differentiable Abstract Interpretation for Provably Robust Neural Networks. In Proc. of ICML. 80. Matthew Mirman, Timon Gehr, and Martin T. Vechev. 2018. Differentiable Abstract Interpretation for Provably Robust Neural Networks. In Proc. of ICML. 80."},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.7794269"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498704"},{"key":"e_1_2_1_43_1","volume":"202","author":"Pabbaraju Chirag","unstructured":"Chirag Pabbaraju , Ezra Winston , and J. Zico Kolter. 202 1. Estimating Lipschitz constants of monotone deep equilibrium models. In Proc. of ICLR. Chirag Pabbaraju, Ezra Winston, and J. Zico Kolter. 2021. Estimating Lipschitz constants of monotone deep equilibrium models. In Proc. of ICLR.","journal-title":"J. Zico Kolter."},{"key":"e_1_2_1_44_1","volume-title":"Proc. of NeurIPS.","author":"Paszke Adam","year":"2019","unstructured":"Adam Paszke , Sam Gross , Francisco Massa , Adam Lerer , James Bradbury , Gregory Chanan , Trevor Killeen , Zeming Lin , Natalia Gimelshein , Luca Antiga , Alban Desmaison , Andreas K\u00f6pf , Edward Yang , Zachary DeVito , Martin Raison , Alykhan Tejani , Sasank Chilamkurthy , Benoit Steiner , Lu Fang , Junjie Bai , and Soumith Chintala . 2019 . PyTorch: An Imperative Style, High-Performance Deep Learning Library . In Proc. of NeurIPS. Adam Paszke, Sam Gross, Francisco Massa, Adam Lerer, James Bradbury, Gregory Chanan, Trevor Killeen, Zeming Lin, Natalia Gimelshein, Luca Antiga, Alban Desmaison, Andreas K\u00f6pf, Edward Yang, Zachary DeVito, Martin Raison, Alykhan Tejani, Sasank Chilamkurthy, Benoit Steiner, Lu Fang, Junjie Bai, and Soumith Chintala. 2019. PyTorch: An Imperative Style, High-Performance Deep Learning Library. In Proc. of NeurIPS."},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38856-9_1"},{"key":"e_1_2_1_46_1","volume-title":"Proc. of NeurIPS.","author":"Raghunathan Aditi","year":"2018","unstructured":"Aditi Raghunathan , Jacob Steinhardt , and Percy Liang . 2018 . Semidefinite relaxations for certifying robustness to adversarial examples . In Proc. of NeurIPS. Aditi Raghunathan, Jacob Steinhardt, and Percy Liang. 2018. Semidefinite relaxations for certifying robustness to adversarial examples. In Proc. of NeurIPS."},{"key":"e_1_2_1_47_1","volume-title":"Manchester","author":"Revay Max","year":"2020","unstructured":"Max Revay , Ruigang Wang , and Ian R . Manchester . 2020 . Lipschitz Bounded Equilibrium Networks. ArXiv preprint, abs\/2010.01732 (2020), https:\/\/doi.org\/10.48550\/arXiv.2010.01732 10.48550\/arXiv.2010.01732 Max Revay, Ruigang Wang, and Ian R. Manchester. 2020. Lipschitz Bounded Equilibrium Networks. ArXiv preprint, abs\/2010.01732 (2020), https:\/\/doi.org\/10.48550\/arXiv.2010.01732"},{"key":"e_1_2_1_48_1","volume-title":"Primer on monotone operator methods. Appl. Comput. Math, 15, 1","author":"Ryu Ernest K","year":"2016","unstructured":"Ernest K Ryu and Stephen Boyd . 2016. Primer on monotone operator methods. Appl. Comput. Math, 15, 1 ( 2016 ). Ernest K Ryu and Stephen Boyd. 2016. Primer on monotone operator methods. Appl. Comput. Math, 15, 1 (2016)."},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1109\/CDC40024.2019.9029363"},{"key":"e_1_2_1_50_1","volume-title":"Proc. Machine Learning and Systems (MLSys).","author":"Serre Fran\u00e7ois","year":"2021","unstructured":"Fran\u00e7ois Serre , Christoph M\u00fcller , Gagandeep Singh , Markus P\u00fcschel , and Martin Vechev . 2021 . Scaling Polyhedral Neural Network Verification on GPUs . In Proc. Machine Learning and Systems (MLSys). Fran\u00e7ois Serre, Christoph M\u00fcller, Gagandeep Singh, Markus P\u00fcschel, and Martin Vechev. 2021. Scaling Polyhedral Neural Network Verification on GPUs. In Proc. Machine Learning and Systems (MLSys)."},{"key":"e_1_2_1_51_1","volume-title":"Vechev","author":"Singh Gagandeep","year":"2019","unstructured":"Gagandeep Singh , Rupanshu Ganvir , Markus P\u00fcschel , and Martin T . Vechev . 2019 . Beyond the Single Neuron Convex Barrier for Neural Network Certification. In Proc. of NeurIPS. Gagandeep Singh, Rupanshu Ganvir, Markus P\u00fcschel, and Martin T. Vechev. 2019. Beyond the Single Neuron Convex Barrier for Neural Network Certification. In Proc. of NeurIPS."},{"key":"e_1_2_1_52_1","volume-title":"Vechev","author":"Singh Gagandeep","year":"2018","unstructured":"Gagandeep Singh , Timon Gehr , Matthew Mirman , Markus P\u00fcschel , and Martin T . Vechev . 2018 . Fast and Effective Robustness Certification. In Proc. of NeurIPS. Gagandeep Singh, Timon Gehr, Matthew Mirman, Markus P\u00fcschel, and Martin T. Vechev. 2018. Fast and Effective Robustness Certification. In Proc. of NeurIPS."},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290354"},{"key":"e_1_2_1_54_1","volume-title":"Proc. of ICLR.","author":"Szegedy Christian","year":"2014","unstructured":"Christian Szegedy , Wojciech Zaremba , Ilya Sutskever , Joan Bruna , Dumitru Erhan , Ian J. Goodfellow , and Rob Fergus . 2014 . Intriguing properties of neural networks . In Proc. of ICLR. Christian Szegedy, Wojciech Zaremba, Ilya Sutskever, Joan Bruna, Dumitru Erhan, Ian J. Goodfellow, and Rob Fergus. 2014. Intriguing properties of neural networks. In Proc. of ICLR."},{"key":"e_1_2_1_55_1","volume-title":"Proc. of NeurIPS.","author":"Tashiro Yusuke","year":"2020","unstructured":"Yusuke Tashiro , Yang Song , and Stefano Ermon . 2020 . Diversity can be Transferred: Output Diversification for White- and Black-box Attacks . In Proc. of NeurIPS. Yusuke Tashiro, Yang Song, and Stefano Ermon. 2020. Diversity can be Transferred: Output Diversification for White- and Black-box Attacks. In Proc. of NeurIPS."},{"key":"e_1_2_1_56_1","volume":"201","author":"Wang Po-Wei","unstructured":"Po-Wei Wang , Priya L. Donti , Bryan Wilder , and J. Zico Kolter. 201 9. SATNet: Bridging deep learning and logical reasoning using a differentiable satisfiability solver. In Proc. of ICML. 97. Po-Wei Wang, Priya L. Donti, Bryan Wilder, and J. Zico Kolter. 2019. SATNet: Bridging deep learning and logical reasoning using a differentiable satisfiability solver. In Proc. of ICML. 97.","journal-title":"J. Zico Kolter."},{"key":"e_1_2_1_57_1","volume-title":"27th USENIX Security Symposium, USENIX Security 2018","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 27th USENIX Security Symposium, USENIX Security 2018 , Baltimore, MD, USA , August 15-17, 2018. Shiqi Wang, Kexin Pei, Justin Whitehouse, Junfeng Yang, and Suman Jana. 2018. Formal Security Analysis of Neural Networks using Symbolic Intervals. In 27th USENIX Security Symposium, USENIX Security 2018, Baltimore, MD, USA, August 15-17, 2018."},{"key":"e_1_2_1_58_1","volume":"202","author":"Wei Colin","unstructured":"Colin Wei and J Zico Kolter. 202 2. Certified Robustness for Deep Equilibrium Models via Interval Bound Propagation. In Proc. of ICLR. Colin Wei and J Zico Kolter. 2022. Certified Robustness for Deep Equilibrium Models via Interval Bound Propagation. In Proc. of ICLR.","journal-title":"J Zico Kolter."},{"key":"e_1_2_1_59_1","volume-title":"Dhillon","author":"Weng Tsui-Wei","year":"2018","unstructured":"Tsui-Wei Weng , Huan Zhang , Hongge Chen , Zhao Song , Cho-Jui Hsieh , Luca Daniel , Duane S. Boning , and Inderjit S . Dhillon . 2018 . Towards Fast Computation of Certified Robustness for ReLU Networks. In Proc. of ICML. 80. Tsui-Wei Weng, Huan Zhang, Hongge Chen, Zhao Song, Cho-Jui Hsieh, Luca Daniel, Duane S. Boning, and Inderjit S. Dhillon. 2018. Towards Fast Computation of Certified Robustness for ReLU Networks. In Proc. of ICML. 80."},{"key":"e_1_2_1_60_1","volume":"202","author":"Winston Ezra","unstructured":"Ezra Winston and J. Zico Kolter. 202 0. Monotone operator equilibrium networks. In Proc. of NeurIPS. Ezra Winston and J. Zico Kolter. 2020. Monotone operator equilibrium networks. In Proc. of NeurIPS.","journal-title":"J. Zico Kolter."},{"key":"e_1_2_1_61_1","volume":"201","author":"Wong Eric","unstructured":"Eric Wong and J. Zico Kolter. 201 8. Provable Defenses against Adversarial Examples via the Convex Outer Adversarial Polytope. In Proc. of ICML. 80. Eric Wong and J. Zico Kolter. 2018. Provable Defenses against Adversarial Examples via the Convex Outer Adversarial Polytope. In Proc. of ICML. 80.","journal-title":"J. Zico Kolter."},{"key":"e_1_2_1_62_1","volume-title":"Proc. of NeurIPS.","author":"Xu Kaidi","year":"2020","unstructured":"Kaidi Xu , Zhouxing Shi , Huan Zhang , Yihan Wang , Kai-Wei Chang , Minlie Huang , Bhavya Kailkhura , Xue Lin , and Cho-Jui Hsieh . 2020 . Automatic Perturbation Analysis for Scalable Certified Robustness and Beyond . In Proc. of NeurIPS. Kaidi Xu, Zhouxing Shi, Huan Zhang, Yihan Wang, Kai-Wei Chang, Minlie Huang, Bhavya Kailkhura, Xue Lin, and Cho-Jui Hsieh. 2020. Automatic Perturbation Analysis for Scalable Certified Robustness and Beyond. In Proc. of NeurIPS."},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.automatica.2018.06.006"},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.23919\/ACC.2004.1383661"},{"key":"e_1_2_1_65_1","volume-title":"Proc. of NeurIPS.","author":"Zhang Huan","year":"2018","unstructured":"Huan Zhang , Tsui-Wei Weng , Pin-Yu Chen , Cho-Jui Hsieh , and Luca Daniel . 2018 . Efficient Neural Network Robustness Certification with General Activation Functions . In Proc. of NeurIPS. Huan Zhang, Tsui-Wei Weng, Pin-Yu Chen, Cho-Jui Hsieh, and Luca Daniel. 2018. Efficient Neural Network Robustness Certification with General Activation Functions. In Proc. of NeurIPS."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3591252","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3591252","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:47:47Z","timestamp":1750178867000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3591252"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,6,6]]},"references-count":66,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2023,6,6]]}},"alternative-id":["10.1145\/3591252"],"URL":"https:\/\/doi.org\/10.1145\/3591252","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,6,6]]},"assertion":[{"value":"2023-06-06","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}