{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,24]],"date-time":"2026-07-24T22:35:21Z","timestamp":1784932521558,"version":"3.55.0"},"publisher-location":"New York, NY, USA","reference-count":36,"publisher":"ACM","license":[{"start":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T00:00:00Z","timestamp":1726012800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"National Key R&D Program of China","award":["No.2022YFA1005101"],"award-info":[{"award-number":["No.2022YFA1005101"]}]},{"name":"National Natural Science Foundation of China","award":["No.62032024"],"award-info":[{"award-number":["No.62032024"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2024,9,11]]},"DOI":"10.1145\/3650212.3680393","type":"proceedings-article","created":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T11:44:25Z","timestamp":1726055065000},"page":"1708-1719","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Synthesizing Boxes Preconditions for Deep Neural Networks"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0007-3896-4971","authenticated-orcid":false,"given":"Zengyu","family":"Liu","sequence":"first","affiliation":[{"name":"State Key Laboratory of Complex & Critical Software Environment, College of Computer Science and Technology, National University of Defense Technology, Changsha, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8084-8009","authenticated-orcid":false,"given":"Liqian","family":"Chen","sequence":"additional","affiliation":[{"name":"State Key Laboratory of Complex & Critical Software Environment, College of Computer Science and Technology, National University of Defense Technology, Changsha, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2315-1704","authenticated-orcid":false,"given":"Wanwei","family":"Liu","sequence":"additional","affiliation":[{"name":"State Key Laboratory of Complex & Critical Software Environment, College of Computer Science and Technology, National University of Defense Technology, Changsha, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0637-8744","authenticated-orcid":false,"given":"Ji","family":"Wang","sequence":"additional","affiliation":[{"name":"State Key Laboratory of Complex & Critical Software Environment, College of Computer Science and Technology, National University of Defense Technology, Changsha, China"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,9,11]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"The 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering.","author":"Ahmed Shibbir","year":"2024","unstructured":"Shibbir Ahmed, Hongyang Gao, and Hridesh Rajan. 2024. Inferring Data Preconditions from Deep Learning Models for Trustworthy Prediction in Deployment. In ICSE\u20192024: The 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314641"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1009951412412"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1561\/2500000002"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE48619.2023.00134"},{"key":"e_1_3_2_1_6_1","volume-title":"Proceedings of the 32nd International Conference on Neural Information Processing Systems (NIPS\u201918)","author":"Bunel Rudy","unstructured":"Rudy Bunel, Ilker Turkaslan, Philip H.S. Torr, Pushmeet Kohli, and M. Pawan Kumar. 2018. A Unified View of Piecewise Linear Neural Network Verification. In Proceedings of the 32nd International Conference on Neural Information Processing Systems (NIPS\u201918). Curran Associates Inc., Red Hook, NY, USA. 4795\u20134804."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICRA.2018.8460487"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-46002-9_14"},{"key":"e_1_3_2_1_9_1","unstructured":"Farama Foundation. 2022. Gym Documentation. https:\/\/www.gymlibrary.dev\/environments\/classic_control\/cart_pole\/"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2019.00079"},{"key":"e_1_3_2_1_11_1","volume-title":"Boxes: A Symbolic Abstract Domain of Boxes","author":"Gurfinkel Arie","year":"2010","unstructured":"Arie Gurfinkel and Sagar Chaki. 2010. Boxes: A Symbolic Abstract Domain of Boxes. In Static Analysis, Radhia Cousot and Matthieu Martel (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 287\u2013303. isbn:978-3-642-15769-1"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"crossref","unstructured":"Anan Kabaha and Dana Drachsler-Cohen. 2023. Maximal Robust Neural Network Specifications via Oracle-Guided Numerical Optimization. In Verification Model Checking and Abstract Interpretation Cezara Dragoi Michael Emmi and Jingbo Wang (Eds.). Springer Nature Switzerland Cham. 203\u2013227. isbn:978-3-031-24950-1","DOI":"10.1007\/978-3-031-24950-1_10"},{"key":"e_1_3_2_1_13_1","volume-title":"Kochenderfer","author":"Katz Guy","year":"2017","unstructured":"Guy Katz, Clark Barrett, David L. Dill, Kyle Julian, and Mykel J. Kochenderfer. 2017. Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. In Computer Aided Verification, Rupak Majumdar and Viktor Kun\u010dak (Eds.). Springer International Publishing, Cham. 97\u2013117. isbn:978-3-319-63387-9"},{"key":"e_1_3_2_1_14_1","volume-title":"Learned Cardinalities: Estimating Correlated Joins with Deep Learning. arxiv:1809.00677.","author":"Kipf Andreas","year":"2018","unstructured":"Andreas Kipf, Thomas Kipf, Bernhard Radke, Viktor Leis, Peter Boncz, and Alfons Kemper. 2018. Learned Cardinalities: Estimating Correlated Joins with Deep Learning. arxiv:1809.00677."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-17244-1_13"},{"key":"e_1_3_2_1_16_1","volume-title":"Provable defenses against adversarial examples via the convex outer adversarial polytope. CoRR, abs\/1711.00851","author":"Zico Kolter J.","year":"2017","unstructured":"J. Zico Kolter and Eric Wong. 2017. Provable defenses against adversarial examples via the convex outer adversarial polytope. CoRR, abs\/1711.00851 (2017), arXiv:1711.00851. arxiv:1711.00851"},{"key":"e_1_3_2_1_17_1","unstructured":"Suhas Kotha Christopher Brix Zico Kolter Krishnamurthy Dvijotham and Huan Zhang. 2023. Provably Bounding Neural Network Preimages. arxiv:2302.01404."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99524-9_16"},{"key":"e_1_3_2_1_19_1","volume-title":"On Certifying Non-uniform Bound against Adversarial Attacks. CoRR, abs\/1903.06603","author":"Liu Chen","year":"2019","unstructured":"Chen Liu, Ryota Tomioka, and Volkan Cevher. 2019. On Certifying Non-uniform Bound against Adversarial Attacks. CoRR, abs\/1903.06603 (2019), arXiv:1903.06603. arxiv:1903.06603"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","unstructured":"Zengyu Liu. 2024. Synthesizing Boxes Preconditions for Deep Neural Networks. https:\/\/doi.org\/10.5281\/zenodo.12673450 10.5281\/zenodo.12673450","DOI":"10.5281\/zenodo.12673450"},{"key":"e_1_3_2_1_21_1","unstructured":"Kyle Matoba. 2020. Exact Preimages of Neural Network Aircraft Collision Avoidance Systems. https:\/\/api.semanticscholar.org\/CorpusID:231854560"},{"key":"e_1_3_2_1_22_1","volume-title":"Johnson","author":"M\u00fcller Mark Niklas","year":"2023","unstructured":"Mark Niklas M\u00fcller, Christopher Brix, Stanley Bak, Changliu Liu, and Taylor T. Johnson. 2023. The Third International Verification of Neural Networks Competition (VNN-COMP 2022): Summary and Results. arxiv:2212.10376."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","unstructured":"Nikhil Naik and Pierluigi Nuzzo. 2020. Robustness Contracts for Scalable Verification of Neural Network-Enabled Cyber-Physical Systems. In 2020 18th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE). 1\u201312. https:\/\/doi.org\/10.1109\/MEMOCODE51338.2020.9315118 10.1109\/MEMOCODE51338.2020.9315118","DOI":"10.1109\/MEMOCODE51338.2020.9315118"},{"key":"e_1_3_2_1_24_1","unstructured":"Th\u00e9o Nancy Vassili Maillet and Johann Barbier. 2022. An Analytical Approach to Compute the Exact Preimage of Feed-Forward Neural Networks. arxiv:2203.00438."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"crossref","unstructured":"Corina Pasareanu Ravi Mangal Divya Gopinath and Huafeng Yu. 2023. Assumption Generation for the Verification of Learning-Enabled Autonomous Systems. arxiv:2305.18372.","DOI":"10.1007\/978-3-031-44267-4_1"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-44267-4_1"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACC.1998.703255"},{"key":"e_1_3_2_1_28_1","volume-title":"Advances in Neural Information Processing Systems","author":"Singh Gagandeep","year":"2018","unstructured":"Gagandeep Singh, Timon Gehr, Matthew Mirman, Markus P\u00fcschel, and Martin Vechev. 2018. Fast and Effective Robustness Certification. In Advances in Neural Information Processing Systems, S. Bengio, H. Wallach, H. Larochelle, K. Grauman, N. Cesa-Bianchi, and R. Garnett (Eds.). 31, Curran Associates, Inc.. https:\/\/proceedings.neurips.cc\/paper_files\/paper\/2018\/file\/f2f446980d8e971ef3da97af089481c3-Paper.pdf"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.5555\/3277203.3277323"},{"key":"e_1_3_2_1_30_1","volume-title":"Beta-CROWN: Efficient bound propagation with per-neuron split constraints for complete and incomplete neural network verification. Advances in Neural Information Processing Systems, 34","author":"Wang Shiqi","year":"2021","unstructured":"Shiqi Wang, Huan Zhang, Kaidi Xu, Xue Lin, Suman Jana, Cho-Jui Hsieh, and J Zico Kolter. 2021. Beta-CROWN: Efficient bound propagation with per-neuron split constraints for complete and incomplete neural network verification. Advances in Neural Information Processing Systems, 34 (2021)."},{"key":"e_1_3_2_1_31_1","volume-title":"Automatic perturbation analysis for scalable certified robustness and beyond. Advances in Neural Information Processing Systems, 33","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. Advances in Neural Information Processing Systems, 33 (2020)."},{"key":"e_1_3_2_1_32_1","unstructured":"Kaidi Xu Huan Zhang Shiqi Wang Yihan Wang Suman Jana Xue Lin and Cho-Jui Hsieh. 2021. Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers. In International Conference on Learning Representations. https:\/\/openreview.net\/forum?id=nVZtXBI6LNn"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/CVPR.2017.148"},{"key":"e_1_3_2_1_35_1","first-page":"4939","article-title":"Efficient Neural Network Robustness Certification with General Activation Functions","volume":"31","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. Advances in Neural Information Processing Systems, 31 (2018), 4939\u20134948. arxiv:1811.00866","journal-title":"Advances in Neural Information Processing Systems"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-57256-2_1"}],"event":{"name":"ISSTA '24: 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis","location":"Vienna Austria","acronym":"ISSTA '24","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering","AITO"]},"container-title":["Proceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3650212.3680393","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3650212.3680393","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T00:58:09Z","timestamp":1750294689000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3650212.3680393"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,9,11]]},"references-count":36,"alternative-id":["10.1145\/3650212.3680393","10.1145\/3650212"],"URL":"https:\/\/doi.org\/10.1145\/3650212.3680393","relation":{},"subject":[],"published":{"date-parts":[[2024,9,11]]},"assertion":[{"value":"2024-09-11","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}