{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T15:30:44Z","timestamp":1743089444321,"version":"3.40.3"},"publisher-location":"Cham","reference-count":75,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031747755"},{"type":"electronic","value":"9783031747762"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-3-031-74776-2_16","type":"book-chapter","created":{"date-parts":[[2025,1,20]],"date-time":"2025-01-20T05:35:09Z","timestamp":1737351309000},"page":"407-424","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["ConstraintFlow: A Declarative DSL for\u00a0Easy Development of\u00a0DNN Certifiers"],"prefix":"10.1007","author":[{"given":"Avaljot","family":"Singh","sequence":"first","affiliation":[]},{"given":"Yasmin","family":"Sarita","sequence":"additional","affiliation":[]},{"given":"Charith","family":"Mendis","sequence":"additional","affiliation":[]},{"given":"Gagandeep","family":"Singh","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,1,21]]},"reference":[{"key":"16_CR1","doi-asserted-by":"crossref","unstructured":"Albarghouthi, A.: Introduction to neural network verification. CoRR abs\/2109.10317 (2021)","DOI":"10.1561\/9781680839111"},{"key":"16_CR2","doi-asserted-by":"crossref","unstructured":"Albarghouthi, A.: Introduction to neural network verification (2021). http:\/\/verifieddeeplearning.com","DOI":"10.1561\/9781680839111"},{"key":"16_CR3","doi-asserted-by":"crossref","unstructured":"Anderson, G., Pailoor, S., Dillig, I., Chaudhuri, S.: Optimization and abstraction: a synergistic approach for analyzing neural network robustness. In: Proceedings of Programming Language Design and Implementation (PLDI), pp. 731\u2013744 (2019)","DOI":"10.1145\/3314221.3314614"},{"key":"16_CR4","doi-asserted-by":"publisher","unstructured":"Boopathy, A., Weng, T.W., Chen, P.Y., Liu, S., Daniel, L.: Cnn-cert: an efficient framework for certifying robustness of convolutional neural networks. In: Proceedings of the Thirty-Third AAAI Conference on Artificial Intelligence and Thirty-First Innovative Applications of Artificial Intelligence Conference and Ninth AAAI Symposium on Educational Advances in Artificial Intelligence, AAAI\u201919\/IAAI\u201919\/EAAI\u201919, AAAI Press (2019). https:\/\/doi.org\/10.1609\/aaai.v33i01.33013240","DOI":"10.1609\/aaai.v33i01.33013240"},{"key":"16_CR5","unstructured":"Brix, C., M\u00fcller, M.N., Bak, S., Johnson, T.T., Liu, C.: First three years of the international verification of neural networks competition (VNN-COMP). CoRR abs\/2301.05815 (2023)"},{"key":"16_CR6","doi-asserted-by":"publisher","unstructured":"Bucur, S., Ureche, V., Zamfir, C., Candea, G.: Parallel symbolic execution for automated real-world software testing. In: Proceedings of the Sixth Conference on Computer Systems, EuroSys 2011, pp. 183\u2013198. Association for Computing Machinery, New York, NY, USA (2011). https:\/\/doi.org\/10.1145\/1966445.1966463","DOI":"10.1145\/1966445.1966463"},{"key":"16_CR7","unstructured":"Cadar, C., Dunbar, D., Engler, D.: Klee: unassisted and automatic generation of high-coverage tests for complex systems programs. In: Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation, OSDI 2008, pp. 209\u2013224. USENIX Association, USA (2008)"},{"key":"16_CR8","doi-asserted-by":"publisher","unstructured":"Cadar, C., Ganesh, V., Pawlowski, P.M., Dill, D.L., Engler, D.R.: Exe: automatically generating inputs of death. In: Proceedings of the 13th ACM Conference on Computer and Communications Security, CCS 2006, pp. 322\u2013335. Association for Computing Machinery, New York, NY, USA (2006). https:\/\/doi.org\/10.1145\/1180405.1180445","DOI":"10.1145\/1180405.1180445"},{"key":"16_CR9","doi-asserted-by":"publisher","unstructured":"Chipounov, V., Kuznetsov, V., Candea, G.: The s2e platform: design, implementation, and applications. ACM Trans. Comput. Syst. 30(1) (2012). https:\/\/doi.org\/10.1145\/2110356.2110358","DOI":"10.1145\/2110356.2110358"},{"key":"16_CR10","doi-asserted-by":"publisher","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL 1977, pp. 238\u2013252. Association for Computing Machinery, New York, NY, USA (1977). https:\/\/doi.org\/10.1145\/512950.512973","DOI":"10.1145\/512950.512973"},{"key":"16_CR11","doi-asserted-by":"publisher","unstructured":"Cousot, P., Cousot, R.: Static determination of dynamic properties of generalized type unions. In: Proceedings of an ACM Conference on Language Design for Reliable Software, pp. 77\u201394. Association for Computing Machinery, New York, NY, USA (1977). https:\/\/doi.org\/10.1145\/800022.808314","DOI":"10.1145\/800022.808314"},{"key":"16_CR12","doi-asserted-by":"publisher","unstructured":"Cousot, P., Giacobazzi, R., Ranzato, F.: A\u0161i: Abstract\u0161 interpretation. Proc. ACM Program. Lang. 3(POPL) (2019). https:\/\/doi.org\/10.1145\/3290355","DOI":"10.1145\/3290355"},{"key":"16_CR13","unstructured":"Guidotti, D., Stefano\u00a0Demarchi, A.T., Pulina, L.: The verification of neural networks library (vnn-lib) (2023). https:\/\/www.vnnlib.org (2023)"},{"key":"16_CR14","unstructured":"D\u2019Souza, D., Ezudheen, P., Garg, P., Madhusudan, P., Neider, D.: Horn-ice learning for synthesizing invariants and contracts. CoRR abs\/1712.09418 (2017). http:\/\/arxiv.org\/abs\/1712.09418"},{"key":"16_CR15","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/978-3-319-77935-5_9","volume-title":"NASA Formal Methods","author":"S Dutta","year":"2018","unstructured":"Dutta, S., Jha, S., Sankaranarayanan, S., Tiwari, A.: Output range analysis for deep feedforward neural networks. In: Dutle, A., Mu\u00f1oz, C., Narkawicz, A. (eds.) NASA Formal Methods, pp. 121\u2013138. Springer International Publishing, Cham (2018)"},{"key":"16_CR16","doi-asserted-by":"crossref","unstructured":"Ehlers, R.: Formal verification of piece-wise linear feed-forward neural networks. In: International Symposium on Automated Technology for Verification and Analysis (2017)","DOI":"10.1007\/978-3-319-68167-2_19"},{"key":"16_CR17","doi-asserted-by":"publisher","unstructured":"Ezudheen, P., Neider, D., D\u2019Souza, D., Garg, P., Madhusudan, P.: Horn-ice learning for synthesizing invariants and contracts. Proc. ACM Program. Lang. 2(OOPSLA), 131:1\u2013131:25 (2018). https:\/\/doi.org\/10.1145\/3276501","DOI":"10.1145\/3276501"},{"key":"16_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/978-3-319-08867-9_5","volume-title":"Computer Aided Verification","author":"P Garg","year":"2014","unstructured":"Garg, P., L\u00f6ding, C., Madhusudan, P., Neider, D.: ICE:\u00a0a\u00a0robust\u00a0framework\u00a0for\u00a0learning\u00a0invariants. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 69\u201387. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_5"},{"key":"16_CR19","doi-asserted-by":"publisher","unstructured":"Gehr, T., Mirman, M., Drachsler-Cohen, D., Tsankov, P., Chaudhuri, S., Vechev, M.T.: AI2: safety and robustness certification of neural networks with abstract interpretation. In: 2018 IEEE Symposium on Security and Privacy, SP 2018, Proceedings, 21\u201323 May 2018, San Francisco, California, USA, pp. 3\u201318 (2018). https:\/\/doi.org\/10.1109\/SP.2018.00058","DOI":"10.1109\/SP.2018.00058"},{"key":"16_CR20","unstructured":"Geng, C., Le, N., Xu, X., Wang, Z., Gurfinkel, A., Si, X.: Towards reliable neural specifications. In: Proceedings of the 40th International Conference on Machine Learning, ICML2023, JMLR.org (2023)"},{"key":"16_CR21","doi-asserted-by":"publisher","unstructured":"Godefroid, P., Klarlund, N., Sen, K.: Dart: Directed automated random testing. In: Proceedings of the 2005 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2005, pp. 213\u2013223. Association for Computing Machinery, New York, NY, USA (2005). https:\/\/doi.org\/10.1145\/1065010.1065036","DOI":"10.1145\/1065010.1065036"},{"key":"16_CR22","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-63387-9_1","volume-title":"Computer Aided Verification","author":"X Huang","year":"2017","unstructured":"Huang, X., Kwiatkowska, M., Wang, S., Wu, M.: Safety verification of deep neural networks. In: Majumdar, R., Kun\u010dak, V. (eds.) Computer Aided Verification, pp. 3\u201329. Springer International Publishing, Cham (2017)"},{"key":"16_CR23","doi-asserted-by":"publisher","unstructured":"Isac, O., Zohar, Y., Barrett, C.W., Katz, G.: DNN verification, reachability, and the exponential function problem. CoRR abs\/2305.06064 (2023). https:\/\/doi.org\/10.48550\/arXiv.2305.06064","DOI":"10.48550\/arXiv.2305.06064"},{"key":"16_CR24","doi-asserted-by":"publisher","first-page":"758","DOI":"10.1007\/978-3-642-31424-7_61","volume-title":"Computer Aided Verification","author":"J Jaffar","year":"2012","unstructured":"Jaffar, J., Murali, V., Navas, J.A., Santosa, A.E.: Tracer: a symbolic execution tool for verification. In: Madhusudan, P., Seshia, S.A. (eds.) Computer Aided Verification, pp. 758\u2013766. Springer, Berlin, Heidelberg (2012)"},{"key":"16_CR25","doi-asserted-by":"publisher","first-page":"396","DOI":"10.1007\/978-3-642-29860-8_32","volume-title":"Runtime Verification","author":"J Jaffar","year":"2012","unstructured":"Jaffar, J., Navas, J.A., Santosa, A.E.: Unbounded symbolic execution for program verification. In: Khurshid, S., Sen, K. (eds.) Runtime Verification, pp. 396\u2013411. Springer, Berlin, Heidelberg (2012)"},{"key":"16_CR26","doi-asserted-by":"publisher","first-page":"454","DOI":"10.1007\/978-3-642-04244-7_37","volume-title":"Principles and Practice of Constraint Programming - CP 2009","author":"J Jaffar","year":"2009","unstructured":"Jaffar, J., Santosa, A.E., Voicu, R.: An interpolation method for clp traversal. In: Gent, I.P. (ed.) Principles and Practice of Constraint Programming - CP 2009, pp. 454\u2013469. Springer, Berlin, Heidelberg (2009)"},{"key":"16_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1007\/978-3-030-25540-4_26","volume-title":"Computer Aided Verification","author":"G Katz","year":"2019","unstructured":"Katz, G., et al.: The marabou framework for verification and analysis of deep neural networks. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 443\u2013452. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_26"},{"key":"16_CR28","doi-asserted-by":"publisher","unstructured":"Keuchel, S., Huyghebaert, S., Lukyanov, G., Devriese, D.: Verified symbolic execution with kripke specification monads (and no meta-programming). Proc. ACM Program. Lang. 6(ICFP) (2022). https:\/\/doi.org\/10.1145\/3547628","DOI":"10.1145\/3547628"},{"key":"16_CR29","doi-asserted-by":"crossref","unstructured":"Li, L., Xie, T., Li, B.: Sok: certified robustness for deep neural networks. In: 44th IEEE Symposium on Security and Privacy, SP 2023, San Francisco, CA, USA, 22\u201326 May 2023. IEEE (2023)","DOI":"10.1109\/SP46215.2023.10179303"},{"key":"16_CR30","doi-asserted-by":"publisher","unstructured":"Lin, Z., Chen, X., Trinh, M.T., Wang, J., Ro\u015fu, G.: Generating proof certificates for a language-agnostic deductive program verifier. Proc. ACM Program. Lang. 7(OOPSLA1) (2023). https:\/\/doi.org\/10.1145\/3586029","DOI":"10.1145\/3586029"},{"key":"16_CR31","doi-asserted-by":"crossref","unstructured":"Logozzo, F., F\u00e4hndrich, M.: Pentagons: A weakly relational abstract domain for the efficient validation of array accesses. Sci. Comput. Program. 75(9), 796\u2013807 (2010). https:\/\/www.sciencedirect.com\/science\/article\/pii\/S0167642309000719, special Issue on Object-Oriented Programming Languages and Systems (OOPS 2008), A Special Track at the 23rd ACM Symposium on Applied Computing","DOI":"10.1016\/j.scico.2009.04.004"},{"key":"16_CR32","doi-asserted-by":"publisher","unstructured":"Lorenz, T., Ruoss, A., Balunovic, M., Singh, G., Vechev, M.: Robustness certification for point cloud models. In: 2021 IEEE\/CVF International Conference on Computer Vision (ICCV), pp. 7588\u20137598. IEEE Computer Society, Los Alamitos, CA, USA, October 2021. https:\/\/doi.org\/10.1109\/ICCV48922.2021.00751","DOI":"10.1109\/ICCV48922.2021.00751"},{"key":"16_CR33","doi-asserted-by":"crossref","unstructured":"Lyu, Z., Ko, C., Kong, Z., Wong, N., Lin, D., Daniel, L.: Fastened CROWN: tightened neural network robustness certificates. In: The Thirty-Fourth AAAI Conference on Artificial Intelligence, AAAI 2020, The Thirty-Second Innovative Applications of Artificial Intelligence Conference, IAAI 2020, The Tenth AAAI Symposium on Educational Advances in Artificial Intelligence, EAAI 2020, New York, NY, USA, 7\u201312 February 2020, pp. 5037\u20135044. AAAI Press (2020). https:\/\/ojs.aaai.org\/index.php\/AAAI\/article\/view\/5944","DOI":"10.1609\/aaai.v34i04.5944"},{"key":"16_CR34","doi-asserted-by":"publisher","first-page":"104","DOI":"10.1007\/978-3-642-14295-6_10","volume-title":"Computer Aided Verification","author":"KL McMillan","year":"2010","unstructured":"McMillan, K.L.: Lazy annotation for program testing and verification. In: Touili, T., Cook, B., Jackson, P. (eds.) Computer Aided Verification, pp. 104\u2013118. Springer, Berlin, Heidelberg (2010)"},{"key":"16_CR35","doi-asserted-by":"publisher","unstructured":"Mine, A.: The octagon abstract domain. In: Proceedings Eighth Working Conference on Reverse Engineering, pp. 310\u2013319 (2001). https:\/\/doi.org\/10.1109\/WCRE.2001.957836","DOI":"10.1109\/WCRE.2001.957836"},{"key":"16_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"16_CR37","unstructured":"M\u00fcller, C., Serre, F., Singh, G., P\u00fcschel, M., Vechev, M.T.: Scaling polyhedral neural network verification on gpus. In: Smola, A., Dimakis, A., Stoica, I. (eds.) Proceedings of Machine Learning and Systems 2021, MLSys 2021, virtual, 5\u20139 April 2021. mlsys.org (2021). https:\/\/proceedings.mlsys.org\/paper\/2021\/hash\/ca46c1b9512a7a8315fa3c5a946e8265-Abstract.html"},{"key":"16_CR38","unstructured":"Pham, L.H., Li, J., Sun, J.: Socrates: towards a unified platform for neural network verification. ArXiv abs\/2007.11206 (2020)"},{"key":"16_CR39","unstructured":"Raghunathan, A., Steinhardt, J., Liang, P.: Semidefinite relaxations for certifying robustness to adversarial examples. In: Proceedings of the 32nd International Conference on Neural Information Processing Systems, NIPS 2018, pp. 10900\u201310910. Curran Associates Inc., Red Hook, NY, USA (2018)"},{"key":"16_CR40","doi-asserted-by":"crossref","unstructured":"Ribeiro, M.T., Singh, S., Guestrin, C.: Why should I trust you?: Explaining the predictions of any classifier. In: Proceedings of ACM SIGKDD International Conference on Knowledge Discovery and Data Mining, pp. 1135\u20131144. ACM (2016)","DOI":"10.1145\/2939672.2939778"},{"key":"16_CR41","volume-title":"A Convex Relaxation Barrier to Tight Robustness Verification of Neural Networks","author":"H Salman","year":"2019","unstructured":"Salman, H., Yang, G., Zhang, H., Hsieh, C.J., Zhang, P.: A Convex Relaxation Barrier to Tight Robustness Verification of Neural Networks. Curran Associates Inc., Red Hook, NY, USA (2019)"},{"key":"16_CR42","doi-asserted-by":"publisher","unstructured":"Sen, K., Marinov, D., Agha, G.: Cute: a concolic unit testing engine for c. In: Proceedings of the 10th European Software Engineering Conference Held Jointly with 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering, ESEC\/FSE-13, pp. 263\u2013272. Association for Computing Machinery, New York, NY, USA (2005). https:\/\/doi.org\/10.1145\/1081706.1081750","DOI":"10.1145\/1081706.1081750"},{"issue":"2","key":"16_CR43","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1109\/MDAT.2020.2971217","volume":"37","author":"M Shafique","year":"2020","unstructured":"Shafique, M., et al.: Robust machine learning systems: challenges, current trends, perspectives, and the road ahead. IEEE Des. Test 37(2), 30\u201357 (2020)","journal-title":"IEEE Des. Test"},{"key":"16_CR44","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1007\/978-3-030-81685-8_6","volume-title":"Computer Aided Verification","author":"D Shriver","year":"2021","unstructured":"Shriver, D., Elbaum, S., Dwyer, M.B.: Dnnv: a framework for deep neural network verification. In: Silva, A., Leino, K.R.M. (eds.) Computer Aided Verification, pp. 137\u2013150. Springer International Publishing, Cham (2021)"},{"key":"16_CR45","unstructured":"Si, X., Dai, H., Raghothaman, M., Naik, M., Song, L.: Learning loop invariants for program verification. In: Bengio, S., Wallach, H., Larochelle, H., Grauman, K., Cesa-Bianchi, N., Garnett, R. (eds.) Advances in Neural Information Processing Systems, vol.\u00a031. Curran Associates, Inc. (2018). https:\/\/proceedings.neurips.cc\/paper_files\/paper\/2018\/file\/65b1e92c585fd4c2159d5f33b5030ff2-Paper.pdf"},{"key":"16_CR46","volume-title":"Beyond the Single Neuron Convex Barrier for Neural Network Certification","author":"G Singh","year":"2019","unstructured":"Singh, G., Ganvir, R., P\u00fcschel, M., Vechev, M.: Beyond the Single Neuron Convex Barrier for Neural Network Certification. Curran Associates Inc., Red Hook, NY, USA (2019)"},{"key":"16_CR47","unstructured":"Singh, G., Gehr, T., Mirman, M., P\u00fcschel, M., Vechev, M.: Fast and effective robustness certification. In: Advances in Neural Information Processing Systems, vol. 31 (2018)"},{"key":"16_CR48","doi-asserted-by":"crossref","unstructured":"Singh, G., Gehr, T., P\u00fcschel, M., Vechev, M.: An abstract domain for certifying neural networks. Proc. ACM Program. Lang. 3(POPL) (2019)","DOI":"10.1145\/3290354"},{"key":"16_CR49","unstructured":"Singh, G., Gehr, T., P\u00fcschel, M., Vechev, M.T.: Boosting robustness certification of neural networks. In: International Conference on Learning Representations (2018)"},{"key":"16_CR50","unstructured":"Singh, G., Gehr, T., P\u00fcschel, M., Vechev, M.T.: ETH robustness analyzer for neural networks (eran) (2018). https:\/\/github.com\/eth-sri\/eran"},{"key":"16_CR51","unstructured":"Singh, G., et al.: Elina: eth library for numerical analysis (2018). https:\/\/github.com\/eth-sri\/ELINA"},{"key":"16_CR52","doi-asserted-by":"publisher","unstructured":"Singh, G., P\u00fcschel, M., Vechev, M.: Making numerical program analysis fast. SIGPLAN Not. 50(6), 303\u2013313 (2015). https:\/\/doi.org\/10.1145\/2813885.2738000","DOI":"10.1145\/2813885.2738000"},{"key":"16_CR53","doi-asserted-by":"publisher","unstructured":"Singh, G., P\u00fcschel, M., Vechev, M.: Fast polyhedra abstract domain. In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, pp. 46\u201359. Association for Computing Machinery, New York, NY, USA (2017). https:\/\/doi.org\/10.1145\/3009837.3009885","DOI":"10.1145\/3009837.3009885"},{"key":"16_CR54","doi-asserted-by":"publisher","unstructured":"Sotoudeh, M., Tao, Z., Thakur, A.: Syrenn: a tool for analyzing deep neural networks. Int. J. Softw. Tools Technol. Transfer 25, 1\u201321 (2023). https:\/\/doi.org\/10.1007\/s10009-023-00695-1","DOI":"10.1007\/s10009-023-00695-1"},{"key":"16_CR55","unstructured":"Szegedy, C., et al.: Intriguing properties of neural networks. In: ICLR (Poster) (2014)"},{"key":"16_CR56","unstructured":"Tjandraatmadja, C., Anderson, R., Huchette, J., Ma, W., Patel, K., Vielma, J.P.: The convex relaxation barrier, revisited: tightened single-neuron relaxations for neural network verification. In: Proceedings of the 34th International Conference on Neural Information Processing Systems. NIPS 2020, Curran Associates Inc., Red Hook, NY, USA (2020)"},{"key":"16_CR57","unstructured":"Tjeng, V., Xiao, K.Y., Tedrake, R.: Evaluating robustness of neural networks with mixed integer programming. In: 7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, 6\u20139 May2019. OpenReview.net (2019). https:\/\/openreview.net\/forum?id=HyGIdiRqtm"},{"key":"16_CR58","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/978-3-030-53288-8_2","volume-title":"Computer Aided Verification","author":"H-D Tran","year":"2020","unstructured":"Tran, H.-D., Bak, S., Xiang, W., Johnson, T.T.: Verification of deep convolutional neural networks using ImageStars. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12224, pp. 18\u201342. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53288-8_2"},{"key":"16_CR59","doi-asserted-by":"publisher","first-page":"670","DOI":"10.1007\/978-3-030-30942-8_39","volume-title":"Formal Methods - The Next 30 Years","author":"HD Tran","year":"2019","unstructured":"Tran, H.D., et al.: Star-based reachability analysis of deep neural networks. In: ter Beek, M.H., McIver, A., Oliveira, J.N. (eds.) Formal Methods - The Next 30 Years, pp. 670\u2013686. Springer International Publishing, Cham (2019)"},{"key":"16_CR60","doi-asserted-by":"publisher","unstructured":"Ugare, S., Banerjee, D., Misailovic, S., Singh, G.: Incremental verification of neural networks. Proc. ACM Program. Lang. 7(PLDI) (2023). https:\/\/doi.org\/10.1145\/3591299","DOI":"10.1145\/3591299"},{"key":"16_CR61","doi-asserted-by":"publisher","unstructured":"Ugare, S., Singh, G., Misailovic, S.: Proof transfer for fast certification of multiple approximate neural networks. Proc. ACM Program. Lang. 6(OOPSLA1) (2022). https:\/\/doi.org\/10.1145\/3527319","DOI":"10.1145\/3527319"},{"key":"16_CR62","doi-asserted-by":"crossref","unstructured":"Vishwanathan, H., Shachnai, M., Narayana, S., Nagarakatte, S.: Verifying the verifier: ebpf range analysis verification. In: Computer Aided Verification (2023)","DOI":"10.1007\/978-3-031-37709-9_12"},{"key":"16_CR63","unstructured":"Wang, S., Pei, K., Whitehouse, J., Yang, J., Jana, S.: Efficient formal safety analysis of neural networks. In: Advances in Neural Information Processing Systems (2018)"},{"key":"16_CR64","unstructured":"Wang, S., Pei, K., Whitehouse, J., Yang, J., Jana, S.: Formal security analysis of neural networks using symbolic intervals. In: Proceedings of the 27th USENIX Conference on Security Symposium, SEC 2018, pp. 1599\u20131614. USENIX Association, USA (2018)"},{"key":"16_CR65","unstructured":"Wang, S., et al.: Beta-crown: efficient bound propagation with per-neuron split constraints for complete and incomplete neural network verification. arXiv preprint arXiv:2103.06624 (2021)"},{"key":"16_CR66","unstructured":"Weng, L., et al.: Towards fast computation of certified robustness for ReLU networks. In: Dy, J., Krause, A. (eds.) Proceedings of the 35th International Conference on Machine Learning. Proceedings of Machine Learning Research, vol.\u00a080, pp. 5276\u20135285. PMLR, 10\u201315 July 2018. https:\/\/proceedings.mlr.press\/v80\/weng18a.html"},{"issue":"10","key":"16_CR67","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1145\/3448248","volume":"64","author":"JM Wing","year":"2021","unstructured":"Wing, J.M.: Trustworthy AI. Commun. ACM 64(10), 64\u201371 (2021)","journal-title":"Commun. ACM"},{"key":"16_CR68","unstructured":"Wong, E., Kolter, J.Z.: Provable defenses against adversarial examples via the convex outer adversarial polytope. In: Dy, J.G., Krause, A. (eds.) Proceedings of the 35th International Conference on Machine Learning, ICML 2018, Stockholmsm\u00e4ssan, Stockholm, Sweden, 10\u201315 July 2018. Proceedings of Machine Learning Research, vol.\u00a080, pp. 5283\u20135292. PMLR (2018). http:\/\/proceedings.mlr.press\/v80\/wong18a.html"},{"key":"16_CR69","doi-asserted-by":"publisher","unstructured":"Wu, H., Barrett, C., Sharif, M., Narodytska, N., Singh, G.: Scalable verification of gnn-based job schedulers. Proc. ACM Program. Lang. 6(OOPSLA2) (2022). https:\/\/doi.org\/10.1145\/3563325","DOI":"10.1145\/3563325"},{"key":"16_CR70","doi-asserted-by":"publisher","unstructured":"Wu, H., et al.: Parallelization techniques for verifying neural networks. In: 2020 Formal Methods in Computer Aided Design (FMCAD), pp. 128\u2013137 (2020). https:\/\/doi.org\/10.34727\/2020\/isbn.978-3-85448-042-6_20","DOI":"10.34727\/2020\/isbn.978-3-85448-042-6_20"},{"key":"16_CR71","unstructured":"Xiang, W., Tran, H., Johnson, T.T.: Output reachable set estimation and verification for multi-layer neural networks. CoRR abs\/1708.03322 (2017), http:\/\/arxiv.org\/abs\/1708.03322"},{"key":"16_CR72","unstructured":"Xu, K., et al.: Automatic perturbation analysis for scalable certified robustness and beyond (2020)"},{"key":"16_CR73","unstructured":"Xu, K., et al.: Fast and complete: enabling complete neural network verification with rapid and massively parallel incomplete verifiers. ArXiv abs\/2011.13824 (2020)"},{"key":"16_CR74","unstructured":"Zelazny, T., Wu, H., Barrett, C.W., Katz, G.: On optimizing back-substitution methods for neural network verification. In: 2022 Formal Methods in Computer-Aided Design (FMCAD), pp. 17\u201326 (2022)"},{"key":"16_CR75","unstructured":"Zhang, H., Weng, T.W., Chen, P.Y., Hsieh, C.J., Daniel, L.: Efficient neural network robustness certification with general activation functions. In: Proceedings of the 32nd International Conference on Neural Information Processing Systems, NIPS 2018, pp. 4944\u20134953. Curran Associates Inc., Red Hook, NY, USA (2018)"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-74776-2_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,20]],"date-time":"2025-01-20T05:35:32Z","timestamp":1737351332000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-74776-2_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031747755","9783031747762"],"references-count":75,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-74776-2_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"21 January 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Static Analysis Symposium","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Pasadena, CA","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 October 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 October 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sas2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/2024.splashcon.org\/home\/sas-2024","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}