{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,14]],"date-time":"2026-03-14T18:07:17Z","timestamp":1773511637883,"version":"3.50.1"},"publisher-location":"Cham","reference-count":129,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031911170","type":"print"},{"value":"9783031911187","type":"electronic"}],"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:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T00:00:00Z","timestamp":1746057600000},"content-version":"vor","delay-in-days":120,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Neural network verification is a new and rapidly developing field of research. So far, the main priority has been establishing efficient verification algorithms and tools, while proper support from the programming language perspective has been considered secondary or unimportant. Yet, there is mounting evidence that insights from the programming language community may make a difference in the future development of this domain. In this paper, we formulate neural network verification challenges as programming language challenges and suggest possible future solutions.<\/jats:p>","DOI":"10.1007\/978-3-031-91118-7_9","type":"book-chapter","created":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T08:17:34Z","timestamp":1746001054000},"page":"206-235","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Neural Network Verification is a Programming Language Challenge"],"prefix":"10.1007","author":[{"given":"Lucas C.","family":"Cordeiro","sequence":"first","affiliation":[]},{"given":"Matthew L.","family":"Daggitt","sequence":"additional","affiliation":[]},{"given":"Julien","family":"Girard-Satabin","sequence":"additional","affiliation":[]},{"given":"Omri","family":"Isac","sequence":"additional","affiliation":[]},{"given":"Taylor T.","family":"Johnson","sequence":"additional","affiliation":[]},{"given":"Guy","family":"Katz","sequence":"additional","affiliation":[]},{"given":"Ekaterina","family":"Komendantskaya","sequence":"additional","affiliation":[]},{"given":"Augustin","family":"Lemesle","sequence":"additional","affiliation":[]},{"given":"Edoardo","family":"Manino","sequence":"additional","affiliation":[]},{"given":"Artjoms","family":"\u0160inkarovs","sequence":"additional","affiliation":[]},{"given":"Haoze","family":"Wu","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,5,1]]},"reference":[{"key":"9_CR1","unstructured":"Open Neural Network Exchange format, https:\/\/onnx.ai\/, accessed on 30.01.2022"},{"key":"9_CR2","unstructured":"Affeldt, R., Bruni, A., Komendantskaya, E., Slusarz, N., Stark, K.: Taming Differentiable Logics with Coq Formalisation. In: Interactive Theorem Provers (ITP) 2024 (2024)"},{"key":"9_CR3","doi-asserted-by":"crossref","unstructured":"Akintunde, M.E., Botoeva, E., Kouvaros, P., Lomuscio, A.: Formal verification of neural agents in non-deterministic environments. In: International Conference on Autonomous Agents and Multiagent Systems, AAMAS. pp. 25\u201333 (2020)","DOI":"10.1007\/s10458-021-09529-3"},{"key":"9_CR4","doi-asserted-by":"crossref","unstructured":"Albarghouthi, A.: Introduction to neural network verification (2021), https:\/\/arxiv.org\/abs\/2109.10317","DOI":"10.1561\/9781680839111"},{"key":"9_CR5","doi-asserted-by":"publisher","unstructured":"Aleksandrov, A., V\u00f6llinger, K.: Formalizing piecewise affine activation functions of neural networks in Coq. In: 15th International NASA Symposium on Formal Methods (NFM 2023), Houston, TX, USA, May 16\u201318, 2023. Lecture Notes in Computer Science, vol. 13903, pp. 62\u201378. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-33170-1_4, https:\/\/doi.org\/10.1007\/978-3-031-33170-1_4","DOI":"10.1007\/978-3-031-33170-1_4 10.1007\/978-3-031-33170-1_4"},{"key":"9_CR6","doi-asserted-by":"crossref","unstructured":"Amir, G., Wu, H., Barrett, C., Katz, G.: An smt-based approach for verifying binarized neural networks. In: Groote, J.F., Larsen, K.G. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. pp. 203\u2013222. Springer International Publishing, Cham (2021)","DOI":"10.1007\/978-3-030-72013-1_11"},{"key":"9_CR7","doi-asserted-by":"publisher","unstructured":"Astorga, A., Hsieh, C., Madhusudan, P., Mitra, S.: Perception contracts for safety of ml-enabled systems. Proc. ACM Program. Lang. 7(OOPSLA2) (Oct 2023). https:\/\/doi.org\/10.1145\/3622875","DOI":"10.1145\/3622875"},{"key":"9_CR8","doi-asserted-by":"crossref","unstructured":"Athavale, A., Bartocci, E., Christakis, M., Maffei, M., Nickovic, D., Weissenbacher, G.: Verifying global two-safety properties in neural networks with confidence (2024), https:\/\/arxiv.org\/abs\/2405.14400","DOI":"10.1007\/978-3-031-65630-9_17"},{"key":"9_CR9","unstructured":"Atkey, R., Daggitt, M.L., Kokke, W.: Vehicle formalisation (2024), https:\/\/github.com\/vehicle-lang\/vehicle-formalisation"},{"key":"9_CR10","doi-asserted-by":"crossref","unstructured":"Bagnall, A., Stewart, G.: Certifying the true error: Machine learning in Coq with verified generalization guarantees. In: Proceedings of the AAAI Conference on Artificial Intelligence. vol.\u00a033, pp. 2662\u20132669 (2019)","DOI":"10.1609\/aaai.v33i01.33012662"},{"key":"9_CR11","unstructured":"Bak, S., Liu, C., Johnson, T.: The Second International Verification of Neural Networks Competition (VNN-COMP 2021): Summary and Results (2021), technical Report. http:\/\/arxiv.org\/abs\/2109.00498"},{"key":"9_CR12","doi-asserted-by":"crossref","unstructured":"Baranowski, M., He, S., Lechner, M., Nguyen, T.S., Rakamari\u0107, Z.: An smt theory of fixed-point arithmetic. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) Automated Reasoning. pp. 13\u201331. Springer International Publishing, Cham (2020)","DOI":"10.1007\/978-3-030-51074-9_2"},{"key":"9_CR13","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org (2016)"},{"key":"9_CR14","doi-asserted-by":"publisher","unstructured":"Baskin, C., Liss, N., Schwartz, E., Zheltonozhskii, E., Giryes, R., Bronstein, A.M., Mendelson, A.: Uniq: Uniform noise injection for non-uniform quantization of neural networks. ACM Trans. Comput. Syst. 37(1\u20134) (mar 2021). https:\/\/doi.org\/10.1145\/3444943, https:\/\/doi.org\/10.1145\/3444943","DOI":"10.1145\/3444943 10.1145\/3444943"},{"key":"9_CR15","doi-asserted-by":"crossref","unstructured":"Beyer, D.: Competition on software verification and witness validation: Sv-comp 2023. In: Sankaranarayanan, S., Sharygina, N. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. pp. 495\u2013522. Springer Nature Switzerland, Cham (2023)","DOI":"10.1007\/978-3-031-30820-8_29"},{"key":"9_CR16","doi-asserted-by":"publisher","unstructured":"Bogomolov, S., Forets, M., Frehse, G., Potomkin, K., Schilling, C.: JuliaReach: A toolbox for set-based reachability. In: Proc. of the 22nd ACM International Conference on Hybrid Systems: Computation and Control. p. 39\u201344 (2019). https:\/\/doi.org\/10.1145\/3302504.3311804","DOI":"10.1145\/3302504.3311804"},{"key":"9_CR17","unstructured":"Brisebarre, N., Hanrot, G., Muller, J.M., Zimmermann, P.: Correctly-rounded evaluation of a function: why, how, and at what cost? (2024), https:\/\/hal.science\/hal-04474530\/document"},{"key":"9_CR18","unstructured":"Brix, C., Bak, S., Johnson, T.T., Wu, H.: The fifth international verification of neural networks competition (vnn-comp 2024): Summary and results (2024), https:\/\/arxiv.org\/abs\/2412.19985"},{"key":"9_CR19","doi-asserted-by":"publisher","unstructured":"Brix, C., Bak, S., Liu, C., Johnson, T.T.: The Fourth International Verification of Neural Networks Competition (VNN-COMP 2023): Summary and Results. CoRR abs\/2312.16760 (2023). https:\/\/doi.org\/10.48550\/ARXIV.2312.16760, https:\/\/doi.org\/10.48550\/arXiv.2312.16760","DOI":"10.48550\/ARXIV.2312.16760"},{"key":"9_CR20","doi-asserted-by":"publisher","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). Int. J. Softw. Tools Technol. Transf. 25(3), 329\u2013339 (2023). https:\/\/doi.org\/10.1007\/S10009-023-00703-4, https:\/\/doi.org\/10.1007\/s10009-023-00703-4","DOI":"10.1007\/S10009-023-00703-4 10.1007\/s10009-023-00703-4"},{"key":"9_CR21","doi-asserted-by":"crossref","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). International Journal on Software Tools for Technology Transfer 25(3), 329\u2013339 (2023)","DOI":"10.1007\/s10009-023-00703-4"},{"key":"9_CR22","doi-asserted-by":"publisher","unstructured":"Brucker, A.D., Stell, A.: Verifying feedforward neural networks for classification in Isabelle\/HOL. In: 25th International Symposium on Formal Methods (FM 2023), L\u00fcbeck, Germany, March 6\u201310, 2023. Lecture Notes in Computer Science, vol. 14000, pp. 427\u2013444. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-27481-7_24, https:\/\/doi.org\/10.1007\/978-3-031-27481-7_24","DOI":"10.1007\/978-3-031-27481-7_24"},{"key":"9_CR23","doi-asserted-by":"publisher","unstructured":"Burgess, N., Milanovic, J., Stephens, N., Monachopoulos, K., Mansell, D.: Bfloat16 processing for neural networks. In: 2019 IEEE 26th Symposium on Computer Arithmetic (ARITH). pp. 88\u201391 (2019). https:\/\/doi.org\/10.1109\/ARITH.2019.00022","DOI":"10.1109\/ARITH.2019.00022"},{"key":"9_CR24","doi-asserted-by":"publisher","unstructured":"Calinescu, R., Imrie, C., Mangal, R., Rodrigues, G.N., P\u0103s\u0103reanu, C., Santana, M.A., V\u00e1zquez, G.: Controller synthesis for autonomous systems with deep-learning perception components. IEEE Transactions on Software Engineering 50(6), 1374\u20131395 (2024). https:\/\/doi.org\/10.1109\/TSE.2024.3385378","DOI":"10.1109\/TSE.2024.3385378"},{"key":"9_CR25","unstructured":"Carlini, N.: A complete list of all (arxiv) adversarial example papers (2019)"},{"key":"9_CR26","doi-asserted-by":"crossref","unstructured":"Casadio, M., Komendantskaya, E., Daggitt, M.L., Kokke, W., Katz, G., Amir, G., Refaeli, I.: Neural network robustness as a verification property: A principled case study. In: Computer Aided Verification (CAV 2022). Lecture Notes in Computer Science, Springer (2022)","DOI":"10.1007\/978-3-031-13185-1_11"},{"key":"9_CR27","doi-asserted-by":"crossref","unstructured":"Casadio, M., Komendantskaya, E., Daggitt, M.L., Kokke, W., Katz, G., Amir, G., Refaeli, I.: Neural network robustness as a verification property: A principled case study. In: Computer Aided Verification (CAV 2022). Lecture Notes in Computer Science, Springer (2022)","DOI":"10.1007\/978-3-031-13185-1_11"},{"key":"9_CR28","doi-asserted-by":"crossref","unstructured":"Christakis, M., Eniser, H.F., Hoffmann, J., Singla, A., W\u00fcstholz, V.: Specifying and testing $$k$$-safety properties for machine-learning models (2022), https:\/\/arxiv.org\/abs\/2206.06054","DOI":"10.24963\/ijcai.2023\/528"},{"key":"9_CR29","unstructured":"Cidon, E., Pergament, E., Asgar, Z., Cidon, A., Katti, S.: Characterizing and taming model instability across edge devices. In: Smola, A., Dimakis, A., Stoica, I. (eds.) Proceedings of Machine Learning and Systems. vol.\u00a03, pp. 624\u2013636 (2021), https:\/\/proceedings.mlsys.org\/paper_files\/paper\/2021\/file\/5190e987c46a346974e351f96997d640-Paper.pdf"},{"key":"9_CR30","unstructured":"Coquand, T., Huet, G.: The calculus of constructions. Ph.D. thesis, Inria (1986)"},{"key":"9_CR31","doi-asserted-by":"publisher","unstructured":"Daggitt, M.L., Kokke, W., Atkey, R., Arnaboldi, L., Komendantskya, E.: Vehicle: Interfacing neural network verifiers with interactive theorem provers (2022). https:\/\/doi.org\/10.48550\/ARXIV.2202.05207, https:\/\/arxiv.org\/abs\/2202.05207","DOI":"10.48550\/ARXIV.2202.05207"},{"key":"9_CR32","doi-asserted-by":"publisher","unstructured":"Daggitt, M.L., Kokke, W., Atkey, R., Slusarz, N., Arnaboldi, L., Komendantskaya, E.: Vehicle: Bridging the embedding gap in the verification of neuro-symbolic programs. CoRR abs\/2401.06379 (2024). https:\/\/doi.org\/10.48550\/ARXIV.2401.06379, https:\/\/doi.org\/10.48550\/arXiv.2401.06379","DOI":"10.48550\/ARXIV.2401.06379 10.48550\/arXiv.2401.06379"},{"key":"9_CR33","doi-asserted-by":"publisher","unstructured":"Daggitt, M.L., Kokke, W., Komendantskaya, E., Atkey, R., Arnaboldi, L., Slusarz, N., Casadio, M., Coke, B., Lee, J.: The vehicle tutorial: Neural network verification with vehicle. In: Narodytska, N., Amir, G., Katz, G., Isac, O. (eds.) Proceedings of the 6th Workshop on Formal Methods for ML-Enabled Autonomous Systems, FoMLAS@CAV 2023, Paris, France, July 17-18, 2023. Kalpa Publications in Computing, vol.\u00a016, pp.\u00a01\u20135. EasyChair (2023). https:\/\/doi.org\/10.29007\/5S2X, https:\/\/doi.org\/10.29007\/5s2x","DOI":"10.29007\/5S2X"},{"key":"9_CR34","doi-asserted-by":"crossref","unstructured":"De\u00a0Maria, E., Bahrami, A., l\u2019Yvonnet, T., Felty, A., Gaff\u00e9, D., Ressouche, A., Grammont, F.: On the use of formal methods to model and verify neuronal archetypes. Frontiers of Computer Science 16(3), 1\u201322 (2022)","DOI":"10.1007\/s11704-020-0029-6"},{"key":"9_CR35","unstructured":"Demarchi, S., Guidotti, D., Pulina, L., Tacchella, A.: Supporting standardization of neural networks verification with vnn-lib and coconet. In: 6th Workshop on Formal Methods for ML-Enabled Autonomous Systems (Jul 2023)"},{"key":"9_CR36","unstructured":"Deng, Z., Meng, G., Chen, K., Liu, T., Xiang, L., Chen, C.: Differential testing of cross deep learning framework APIs: Revealing inconsistencies and vulnerabilities. In: 32nd USENIX Security Symposium (USENIX Security 23). pp. 7393\u20137410. USENIX Association, Anaheim, CA (Aug 2023), https:\/\/www.usenix.org\/conference\/usenixsecurity23\/presentation\/deng-zizhuang"},{"key":"9_CR37","doi-asserted-by":"crossref","unstructured":"Desmartin, R., Isac, O., Komendantskaya, E., Stark, K., Passmore, G., Katz, G.: A Certified Proof Checker for Deep Neural Network Verification. In: https:\/\/arxiv.org\/abs\/2405.10611 (2024)","DOI":"10.1007\/978-3-031-45784-5_13"},{"key":"9_CR38","doi-asserted-by":"publisher","unstructured":"Desmartin, R., Isac, O., Passmore, G.O., Stark, K., Komendantskaya, E., Katz, G.: Towards a Certified Proof Checker for Deep Neural Network Verification. In: Gl\u00fcck, R., Kafle, B. (eds.) Logic-Based Program Synthesis and Transformation - 33rd International Symposium, LOPSTR 2023, Cascais, Portugal, October 23-24, 2023, Proceedings. Lecture Notes in Computer Science, vol. 14330, pp. 198\u2013209. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-45784-5_13, https:\/\/doi.org\/10.1007\/978-3-031-45784-5_13","DOI":"10.1007\/978-3-031-45784-5_13"},{"key":"9_CR39","doi-asserted-by":"publisher","unstructured":"Desmartin, R., Passmore, G.O., Komendantskaya, E., Daggit, M.: Checkinn: Wide range neural network verification in imandra. In: PPDP 2022: 24th International Symposium on Principles and Practice of Declarative Programming, Tbilisi, Georgia, September 20 - 22, 2022. pp. 3:1\u20133:14. ACM (2022). https:\/\/doi.org\/10.1145\/3551357.3551372, https:\/\/doi.org\/10.1145\/3551357.3551372","DOI":"10.1145\/3551357.3551372"},{"key":"9_CR40","doi-asserted-by":"publisher","unstructured":"Dutta, S., Chen, X., Sankaranarayanan, S.: Reachability analysis for neural feedback systems using regressive polynomial rule inference. In: ACM International Conference on Hybrid Systems: Computation and Control, HSCC. pp. 157\u2013168 (2019). https:\/\/doi.org\/10.1145\/3302504.3311807","DOI":"10.1145\/3302504.3311807"},{"key":"9_CR41","doi-asserted-by":"publisher","unstructured":"Dutta, S., Jha, S., Sankaranarayanan, S., Tiwari, A.: Learning and verification of feedback control systems using feedforward neural networks. IFAC-PapersOnLine 51(16), 151 \u2013 156 (2018). https:\/\/doi.org\/10.1016\/j.ifacol.2018.08.026, iFAC Conference on Analysis and Design of Hybrid Systems ADHS 2018","DOI":"10.1016\/j.ifacol.2018.08.026"},{"key":"9_CR42","doi-asserted-by":"crossref","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)","DOI":"10.1007\/978-3-319-77935-5_9"},{"key":"9_CR43","doi-asserted-by":"crossref","unstructured":"Ehlers, R.: Formal verification of piece-wise linear feed-forward neural networks. In: D\u2019Souza, D., Narayan\u00a0Kumar, K. (eds.) Automated Technology for Verification and Analysis. pp. 269\u2013286. Springer International Publishing, Cham (2017)","DOI":"10.1007\/978-3-319-68167-2_19"},{"key":"9_CR44","doi-asserted-by":"crossref","unstructured":"Fan, J., Huang, C., Li, W., Chen, X., Zhu, Q.: Reachnn*: A tool for reachability analysis ofneural-network controlled systems. In: International Symposium on Automated Technology for Verification and Analysis (ATVA) (2020)","DOI":"10.1007\/978-3-030-59152-6_30"},{"key":"9_CR45","doi-asserted-by":"publisher","unstructured":"Filli\u00e2tre, J.C., Paskevich, A.: Why3 - Where Programs Meet Provers. In: Felleisen, M., Gardner, P. (eds.) Programming Languages and Systems. pp. 125\u2013128. Lecture Notes in Computer Science, Springer, Berlin, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-37036-6_8","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"9_CR46","unstructured":"Fischer, M., Balunovic, M., Drachsler-Cohen, D., Gehr, T., Zhang, C., Vechev, M.T.: DL2: training and querying neural networks with logic. In: Chaudhuri, K., Salakhutdinov, R. (eds.) Proceedings of the 36th International Conference on Machine Learning, ICML 2019, 9-15 June 2019, Long Beach, California, USA. Proceedings of Machine Learning Research, vol.\u00a097, pp. 1931\u20131941. PMLR (2019), http:\/\/proceedings.mlr.press\/v97\/fischer19a.html"},{"key":"9_CR47","doi-asserted-by":"crossref","unstructured":"Flinkow, T., Pearlmutter, B.A., Monahan, R.: Comparing differentiable logics for learning with logical constraints (2024), https:\/\/arxiv.org\/abs\/2407.03847","DOI":"10.1016\/j.scico.2025.103280"},{"key":"9_CR48","doi-asserted-by":"publisher","unstructured":"Fremont, D.J., Dreossi, T., Ghosh, S., Yue, X., Sangiovanni-Vincentelli, A.L., Seshia, S.A.: Scenic: a language for scenario specification and scene generation. In: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. p. 63\u201378. PLDI 2019, Association for Computing Machinery, New York, NY, USA (2019).https:\/\/doi.org\/10.1145\/3314221.3314633","DOI":"10.1145\/3314221.3314633"},{"key":"9_CR49","doi-asserted-by":"crossref","unstructured":"Gholami, A., Kim, S., Dong, Z., Yao, Z., Mahoney, M.W., Keutzer, K.: A survey of quantization methods for efficient neural network inference. In: Low-Power Computer Vision, pp. 291\u2013326. Chapman and Hall\/CRC (2022)","DOI":"10.1201\/9781003162810-13"},{"key":"9_CR50","doi-asserted-by":"crossref","unstructured":"Giacobbe, M., Henzinger, T.A., Lechner, M.: How many bits does it take to quantize your neural network? In: Biere, A., Parker, D. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. pp. 79\u201397. Springer International Publishing, Cham (2020)","DOI":"10.26226\/morressier.604907f51a80aac83ca25da2"},{"key":"9_CR51","unstructured":"Girard-Satabin, J., Alberti, M., Bobot, F., Chihani, Z., Lemesle, A.: Caisar: A platform for characterizing artificial intelligence safety and robustness. In: AISafety. CEUR-Workshop Proceedings, Vienne, Austria (Jul 2022), https:\/\/hal.archives-ouvertes.fr\/hal-03687211"},{"key":"9_CR52","doi-asserted-by":"publisher","unstructured":"Giunchiglia, E., Stoian, M.C., Lukasiewicz, T.: Deep learning with logical constraints. In: Thirty-First International Joint Conference on Artificial Intelligence (IJCAI-22). pp. 5478\u20135485. International Joint Conferences on Artificial Intelligence Organization (7 2022). https:\/\/doi.org\/10.24963\/ijcai.2022\/767, https:\/\/doi.org\/10.24963\/ijcai.2022\/767, survey Track","DOI":"10.24963\/ijcai.2022\/767"},{"key":"9_CR53","doi-asserted-by":"publisher","unstructured":"Giunchiglia, E., Stoian, M.C., Lukasiewicz, T.: Deep learning with logical constraints. In: Raedt, L.D. (ed.) Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence, IJCAI 2022, Vienna, Austria, 23-29 July 2022. pp. 5478\u20135485. ijcai.org (2022). https:\/\/doi.org\/10.24963\/ijcai.2022\/767, https:\/\/doi.org\/10.24963\/ijcai.2022\/767","DOI":"10.24963\/ijcai.2022\/767"},{"key":"9_CR54","unstructured":"Goodfellow, I.J., Shlens, J., Szegedy, C.: Explaining and harnessing adversarial examples (2015)"},{"key":"9_CR55","doi-asserted-by":"crossref","unstructured":"Gowal, S., Dvijotham, K.D., Stanforth, R., Bunel, R., Qin, C., Uesato, J., Arandjelovic, R., Mann, T., Kohli, P.: Scalable verified training for provably robust image classification. In: Proceedings of the IEEE\/CVF International Conference on Computer Vision. pp. 4842\u20134851 (2019)","DOI":"10.1109\/ICCV.2019.00494"},{"key":"9_CR56","doi-asserted-by":"publisher","unstructured":"Guo, Q., Xie, X., Li, Y., Zhang, X., Liu, Y., Li, X., Shen, C.: Audee: Automated testing for deep learning frameworks. In: Proceedings of the 35th IEEE\/ACM International Conference on Automated Software Engineering. p. 486\u2013498. ASE \u201920, Association for Computing Machinery, New York, NY, USA (2021). https:\/\/doi.org\/10.1145\/3324884.3416571, https:\/\/doi.org\/10.1145\/3324884.3416571","DOI":"10.1145\/3324884.3416571"},{"key":"9_CR57","doi-asserted-by":"publisher","unstructured":"Hatcliff, J., Leavens, G.T., Leino, K.R.M., M\u00fcller, P., Parkinson, M.: Behavioral interface specification languages. ACM Comput. Surv. 44(3) (Jun 2012). https:\/\/doi.org\/10.1145\/2187671.2187678, https:\/\/doi.org\/10.1145\/2187671.2187678","DOI":"10.1145\/2187671.2187678 10.1145\/2187671.2187678"},{"key":"9_CR58","doi-asserted-by":"crossref","unstructured":"He, Z., Fan, D.: Simultaneously optimizing weight and quantizer of ternary neural network using truncated gaussian approximation. In: Proceedings of the IEEE\/CVF Conference on Computer Vision and Pattern Recognition (CVPR) (June 2019)","DOI":"10.1109\/CVPR.2019.01170"},{"key":"9_CR59","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Lechner, M., \u017dikeli\u0107, \u0110.: Scalable verification of quantized neural networks. In: Proceedings of the AAAI conference on artificial intelligence. vol.\u00a035, pp. 3787\u20133795 (2021)","DOI":"10.1609\/aaai.v35i5.16496"},{"key":"9_CR60","doi-asserted-by":"crossref","unstructured":"Hitzler, P., Sarker, M.: Neuro-symbolic Artificial Intelligence: The State of the Art. IOS Press (2022)","DOI":"10.3233\/FAIA342"},{"key":"9_CR61","doi-asserted-by":"crossref","unstructured":"Huang, C., Fan, J., Chen, X., Li, W., Zhu, Q.: POLAR: A polynomial arithmetic framework for verifying neural-network controlled systems. In: International Symposium on Automated Technology for Verification and Analysis (ATVA) (2022)","DOI":"10.1007\/978-3-031-19992-9_27"},{"key":"9_CR62","doi-asserted-by":"crossref","unstructured":"Huang, C., Fan, J., Li, W., Chen, X., Zhu, Q.: Reachnn: Reachability analysis of neural-network controlled systems. ACM Transactions on Embedded Computing Systems (TECS) 18(5s), 1\u201322 (2019)","DOI":"10.1145\/3358228"},{"key":"9_CR63","doi-asserted-by":"crossref","unstructured":"Huang, P., Wu, H., Yang, Y., Daukantas, I., Wu, M., Zhang, Y., Barrett, C.: Towards efficient verification of quantized neural networks. In: Proceedings of the AAAI Conference on Artificial Intelligence. vol.\u00a038, pp. 21152\u201321160 (2024)","DOI":"10.1609\/aaai.v38i19.30108"},{"key":"9_CR64","doi-asserted-by":"crossref","unstructured":"Huang, X., Kwiatkowska, M., Wang, S., Wu, M.: Safety verification of deep neural networks (2017)","DOI":"10.1007\/978-3-319-63387-9_1"},{"key":"9_CR65","doi-asserted-by":"publisher","unstructured":"IEEE: Ieee standard for floating-point arithmetic. IEEE Std 754-2019 (Revision of IEEE 754-2008) pp. 1\u201384 (2019). https:\/\/doi.org\/10.1109\/IEEESTD.2019.8766229","DOI":"10.1109\/IEEESTD.2019.8766229"},{"key":"9_CR66","unstructured":"Isac, O., Barrett, C., Zhang, M., Katz, G.: Neural Network Verification with Proof Production. In: Proc. 22nd Int. Conf. on Formal Methods in Computer-Aided Design (FMCAD). pp. 38\u201348 (2022)"},{"key":"9_CR67","doi-asserted-by":"crossref","unstructured":"Ivanov, R., Carpenter, T., Weimer, J., Alur, R., Pappas, G.J., Lee, I.: Verisig 2.0: Verification of neural network controllers using taylor model preconditioning. In: International Conference on Computer-Aided Verification (2021)","DOI":"10.1007\/978-3-030-81685-8_11"},{"key":"9_CR68","doi-asserted-by":"publisher","unstructured":"Ivanov, R., Carpenter, T.J., Weimer, J., Alur, R., Pappas, G.J., Lee, I.: Verifying the safety of autonomous systems with neural network controllers. ACM Trans. Embed. Comput. Syst. 20(1) (Dec 2020). https:\/\/doi.org\/10.1145\/3419742","DOI":"10.1145\/3419742"},{"key":"9_CR69","doi-asserted-by":"publisher","unstructured":"Ivanov, R., Weimer, J., Alur, R., Pappas, G.J., Lee, I.: Verisig: Verifying safety properties of hybrid systems with neural network controllers. In: International Conference on Hybrid Systems: Computation and Control. p. 169\u2013178. HSCC, ACM (2019). https:\/\/doi.org\/10.1145\/3302504.3311806","DOI":"10.1145\/3302504.3311806"},{"key":"9_CR70","unstructured":"Jia, K., Rinard, M.: Efficient exact verification of binarized neural networks. In: Larochelle, H., Ranzato, M., Hadsell, R., Balcan, M., Lin, H. (eds.) Advances in Neural Information Processing Systems. vol.\u00a033, pp. 1782\u20131795. Curran Associates, Inc. (2020), https:\/\/proceedings.neurips.cc\/paper_files\/paper\/2020\/file\/1385974ed5904a438616ff7bdb3f7439-Paper.pdf"},{"key":"9_CR71","doi-asserted-by":"crossref","unstructured":"Jia, K., Rinard, M.: Exploiting verified neural networks via floating point numerical error. In: Dr\u0103goi, C., Mukherjee, S., Namjoshi, K. (eds.) Static Analysis. pp. 191\u2013205. Springer International Publishing, Cham (2021)","DOI":"10.1007\/978-3-030-88806-0_9"},{"key":"9_CR72","doi-asserted-by":"publisher","unstructured":"Johnson, T.T., Lopez, D.M., Benet, L., Forets, M., Guadalupe, S., Schilling, C., Ivanov, R., Carpenter, T.J., Weimer, J., Lee, I.: Arch-comp21 category report: Artificial intelligence and neural network control systems (ainncs) for continuous and hybrid systems plants. In: Frehse, G., Althoff, M. (eds.) 8th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH21). EPiC Series in Computing, vol.\u00a080, pp. 90\u2013119. EasyChair (2021). https:\/\/doi.org\/10.29007\/kfk9, https:\/\/easychair.org\/publications\/paper\/Jq4h","DOI":"10.29007\/kfk9"},{"key":"9_CR73","doi-asserted-by":"publisher","unstructured":"Johnson, T.T., Lopez, D.M., Musau, P., Tran, H.D., Botoeva, E., Leofante, F., Maleki, A., Sidrane, C., Fan, J., Huang, C.: Arch-comp20 category report: Artificial intelligence and neural network control systems (ainncs) for continuous and hybrid systems plants. In: Frehse, G., Althoff, M. (eds.) ARCH20. 7th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH20). EPiC Series in Computing, vol.\u00a074, pp. 107\u2013139. EasyChair (2020). https:\/\/doi.org\/10.29007\/9xgv, https:\/\/easychair.org\/publications\/paper\/Jvwg","DOI":"10.29007\/9xgv"},{"key":"9_CR74","doi-asserted-by":"crossref","unstructured":"Katz, G., Barrett, C., Dill, D.L., Julian, K., Kochenderfer, M.J.: Reluplex: An efficient smt solver for verifying deep neural networks. In: International conference on computer aided verification. pp. 97\u2013117. Springer (2017)","DOI":"10.1007\/978-3-319-63387-9_5"},{"key":"9_CR75","doi-asserted-by":"crossref","unstructured":"Katz, G., Huang, D., Ibeling, D., Julian, K., Lazarus, C., Lim, R., Shah, P., Thakoor, S., Wu, H., Zelji\u0107, A., Dill, D., Kochenderfer, M., Barrett, C.: The Marabou Framework for Verification and Analysis of Deep Neural Networks, pp. 443\u2013452 (07 2019)","DOI":"10.1007\/978-3-030-25540-4_26"},{"key":"9_CR76","doi-asserted-by":"crossref","unstructured":"Kochdumper, N., Schilling, C., Althoff, M., Bak, S.: Open- and closed-loop neural network verification using polynomial zonotopes. In: NASA Formal Methods. pp. 16\u201336. Springer (2023)","DOI":"10.1007\/978-3-031-33170-1_2"},{"key":"9_CR77","doi-asserted-by":"publisher","unstructured":"Kokke, W., Komendantskaya, E., Kienitz, D., Atkey, R., Aspinall, D.: Neural networks, secure by construction - an exploration of refinement types. In: d.\u00a0S.\u00a0Oliveira, B.C. (ed.) Programming Languages and Systems - 18th Asian Symposium, APLAS 2020, Fukuoka, Japan, November 30 - December 2, 2020, Proceedings. Lecture Notes in Computer Science, vol. 12470, pp. 67\u201385. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-64437-6_4, https:\/\/doi.org\/10.1007\/978-3-030-64437-6_4","DOI":"10.1007\/978-3-030-64437-6_4 10.1007\/978-3-030-64437-6_4"},{"key":"9_CR78","unstructured":"Kolter, Z., Madry, A.: Adversarial robustness\u2014theory and practice. NeurIPS 2018 tutorial (2018), available at https:\/\/adversarial-ml-tutorial.org\/"},{"key":"9_CR79","unstructured":"Kolter, Z., Madry, A.: Adversarial robustness: Theory and practice. Tutorial at NeurIPS p.\u00a03 (2018)"},{"key":"9_CR80","doi-asserted-by":"crossref","unstructured":"Kroening, D., Tautschnig, M.: CBMC\u2013C bounded model checker. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems. pp. 389\u2013391. Springer (2014)","DOI":"10.1007\/978-3-642-54862-8_26"},{"key":"9_CR81","unstructured":"Li, Y., Dong, X., Wang, W.: Additive powers-of-two quantization: An efficient non-uniform discretization for neural networks. In: International Conference on Learning Representations (2020), https:\/\/openreview.net\/forum?id=BkgXT24tDS"},{"key":"9_CR82","doi-asserted-by":"publisher","unstructured":"Lohar, D., Jeangoudoux, C., Volkova, A., Darulova, E.: Sound mixed fixed-point quantization of neural networks. ACM Trans. Embed. Comput. Syst. 22(5s) (sep 2023). https:\/\/doi.org\/10.1145\/3609118, https:\/\/doi.org\/10.1145\/3609118","DOI":"10.1145\/3609118 10.1145\/3609118"},{"key":"9_CR83","doi-asserted-by":"publisher","unstructured":"Lopez, D.M., Althoff, M., Benet, L., Chen, X., Fan, J., Forets, M., Huang, C., Johnson, T.T., Ladner, T., Li, W., Schilling, C., Zhu, Q.: Arch-comp22 category report: Artificial intelligence and neural network control systems (ainncs) for continuous and hybrid systems plants. In: Frehse, G., Althoff, M., Schoitsch, E., Guiochet, J. (eds.) Proceedings of 9th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH22). EPiC Series in Computing, vol.\u00a090, pp. 142\u2013184. EasyChair (2022). https:\/\/doi.org\/10.29007\/wfgr, https:\/\/easychair.org\/publications\/paper\/C1J8","DOI":"10.29007\/wfgr"},{"key":"9_CR84","doi-asserted-by":"publisher","unstructured":"Lopez, D.M., Althoff, M., Forets, M., Johnson, T.T., Ladner, T., Schilling, C.: Arch-comp23 category report: Artificial intelligence and neural network control systems (ainncs) for continuous and hybrid systems plants. In: Frehse, G., Althoff, M. (eds.) Proceedings of 10th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH23). EPiC Series in Computing, vol.\u00a096, pp. 89\u2013125. EasyChair (2023). https:\/\/doi.org\/10.29007\/x38n","DOI":"10.29007\/x38n"},{"key":"9_CR85","doi-asserted-by":"crossref","unstructured":"Lopez, D.M., Choi, S.W., Tran, H.D., Johnson, T.T.: NNV 2.0: The neural network verification tool. In: Enea, C., Lal, A. (eds.) Computer Aided Verification. pp. 397\u2013412. Springer Nature Switzerland, Cham (2023)","DOI":"10.1007\/978-3-031-37703-7_19"},{"key":"9_CR86","doi-asserted-by":"publisher","unstructured":"Lopez, D.M., Musau, P., Tran, H.D., Dutta, S., Carpenter, T.J., Ivanov, R., Johnson, T.T.: Arch-comp19 category report: Artificial intelligence and neural network control systems (ainncs) for continuous and hybrid systems plants. In: Frehse, G., Althoff, M. (eds.) ARCH19. 6th International Workshop on Applied Verification of Continuous and Hybrid Systems. EPiC Series in Computing, vol.\u00a061, pp. 103\u2013119. EasyChair (2019). https:\/\/doi.org\/10.29007\/rgv8, https:\/\/easychair.org\/publications\/paper\/BFKs","DOI":"10.29007\/rgv8"},{"key":"9_CR87","unstructured":"Madry, A., Makelov, A., Schmidt, L., Tsipras, D., Vladu, A.: Towards deep learning models resistant to adversarial attacks. In: International Conference on Learning Representations (2018)"},{"key":"9_CR88","doi-asserted-by":"publisher","unstructured":"Magalh\u00e3es, J.W.d.S., Woodruff, J., Polgreen, E., O\u2019Boyle, M.F.P.: C2taco: Lifting tensor code to taco. In: Proceedings of the 22nd ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences. p. 42-56. GPCE 2023, Association for Computing Machinery, New York, NY, USA (2023). https:\/\/doi.org\/10.1145\/3624007.3624053, https:\/\/doi.org\/10.1145\/3624007.3624053","DOI":"10.1145\/3624007.3624053 10.1145\/3624007.3624053"},{"key":"9_CR89","doi-asserted-by":"publisher","unstructured":"Mandal, U., Amir, G., Wu, H., Daukantas, I., Newell, F.L., Ravaioli, U.J., Meng, B., Durling, M., Ganai, M., Shim, T., Katz, G., Barrett, C.W.: Formally verifying deep reinforcement learning controllers with lyapunov barrier certificates. CoRR abs\/2405.14058 (2024). https:\/\/doi.org\/10.48550\/ARXIV.2405.14058, https:\/\/doi.org\/10.48550\/arXiv.2405.14058","DOI":"10.48550\/ARXIV.2405.14058 10.48550\/arXiv.2405.14058"},{"key":"9_CR90","doi-asserted-by":"publisher","unstructured":"Manhaeve, R., Duman\u010di\u0107, S., Kimmig, A., Demeester, T., De Raedt, L.: Neural probabilistic logic programming in deepproblog. Artificial Intelligence 298, 103504 (2021). https:\/\/doi.org\/10.1016\/j.artint.2021.103504, https:\/\/www.sciencedirect.com\/science\/article\/pii\/S0004370221000552","DOI":"10.1016\/j.artint.2021.103504"},{"key":"9_CR91","unstructured":"Manino, E., Menezes, R.S., Shmarov, F., Cordeiro, L.C.: NeuroCodeBench: a Plain C Neural Network Benchmark for Software Verification. In: Workshop on Automated Formal Reasoning for Trustworthy AI Systems (2023)"},{"key":"9_CR92","doi-asserted-by":"publisher","unstructured":"Matos, J.B.P., de\u00a0Lima\u00a0Filho, E.B., Bessa, I., Manino, E., Song, X., Cordeiro, L.C.: Counterexample guided neural network quantization refinement. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 43(4), 1121\u20131134 (2024). https:\/\/doi.org\/10.1109\/TCAD.2023.3335313","DOI":"10.1109\/TCAD.2023.3335313"},{"key":"9_CR93","doi-asserted-by":"crossref","unstructured":"Menezes, R.S., Aldughaim, M., Farias, B., Li, X., Manino, E., Shmarov, F., Song, K., Brau\u00dfe, F., Gadelha, M.R., Tihanyi, N., Korovin, K., Cordeiro, L.C.: Esbmc v7.4: Harnessing the power of intervals. In: Finkbeiner, B., Kov\u00e1cs, L. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. pp. 376\u2013380. Springer Nature Switzerland, Cham (2024)","DOI":"10.1007\/978-3-031-57256-2_24"},{"key":"9_CR94","doi-asserted-by":"publisher","unstructured":"Mistry, S., Saha, I., Biswas, S.: An milp encoding for efficient verification of quantized deep neural networks. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 41(11), 4445\u20134456 (2022). https:\/\/doi.org\/10.1109\/TCAD.2022.3197697","DOI":"10.1109\/TCAD.2022.3197697"},{"key":"9_CR95","doi-asserted-by":"crossref","unstructured":"Murphy, C., Gray, P., Stewart, G.: Verified perceptron convergence theorem. In: Proceedings of the 1st ACM SIGPLAN International Workshop on Machine Learning and Programming Languages. pp. 43\u201350 (2017)","DOI":"10.1145\/3088525.3088673"},{"key":"9_CR96","unstructured":"M\u00fcller, M.N., Eckert, F., Fischer, M., Vechev, M.: Certified training: Small boxes are all you need (2023)"},{"key":"9_CR97","doi-asserted-by":"crossref","unstructured":"Narodytska, N., Kasiviswanathan, S., Ryzhyk, L., Sagiv, M., Walsh, T.: Verifying properties of binarized deep neural networks. In: Proceedings of the AAAI Conference on Artificial Intelligence. vol.\u00a032 (2018)","DOI":"10.1609\/aaai.v32i1.12206"},{"key":"9_CR98","unstructured":"Odena, A., Olsson, C., Andersen, D., Goodfellow, I.: TensorFuzz: Debugging neural networks with coverage-guided fuzzing. In: Chaudhuri, K., Salakhutdinov, R. (eds.) Proceedings of the 36th International Conference on Machine Learning. Proceedings of Machine Learning Research, vol.\u00a097, pp. 4901\u20134911. PMLR (09\u201315 Jun 2019), https:\/\/proceedings.mlr.press\/v97\/odena19a.html"},{"key":"9_CR99","doi-asserted-by":"publisher","unstructured":"Payani, A., Fekri, F.: Inductive Logic Programming via Differentiable Deep Neural Logic Networks. Tech. rep. (Jun 2019). https:\/\/doi.org\/10.48550\/arXiv.1906.03523, http:\/\/arxiv.org\/abs\/1906.03523, zSCC: 0000039 arXiv:1906.03523 [cs] type: article","DOI":"10.48550\/arXiv.1906.03523"},{"key":"9_CR100","doi-asserted-by":"publisher","unstructured":"Pham, H.V., Qian, S., Wang, J., Lutellier, T., Rosenthal, J., Tan, L., Yu, Y., Nagappan, N.: Problems and opportunities in training deep learning software systems: an analysis of variance. In: Proceedings of the 35th IEEE\/ACM International Conference on Automated Software Engineering. p. 771\u2013783. ASE \u201920, Association for Computing Machinery, New York, NY, USA (2021). https:\/\/doi.org\/10.1145\/3324884.3416545, https:\/\/doi.org\/10.1145\/3324884.3416545","DOI":"10.1145\/3324884.3416545 10.1145\/3324884.3416545"},{"key":"9_CR101","doi-asserted-by":"crossref","unstructured":"Prach, B., Brau, F., Buttazzo, G., Lampert, C.H.: 1-lipschitz layers compared: Memory speed and certifiable robustness. In: Proceedings of the IEEE\/CVF Conference on Computer Vision and Pattern Recognition (CVPR). pp. 24574\u201324583 (June 2024)","DOI":"10.1109\/CVPR52733.2024.02320"},{"key":"9_CR102","doi-asserted-by":"crossref","unstructured":"Pulina, L., Tacchella, A.: An abstraction-refinement approach to verification of artificial neural networks. In: Touili, T., Cook, B., Jackson, P. (eds.) Computer Aided Verification. pp. 243\u2013257. Springer Berlin Heidelberg, Berlin, Heidelberg (2010)","DOI":"10.1007\/978-3-642-14295-6_24"},{"key":"9_CR103","doi-asserted-by":"publisher","unstructured":"Qin, H., Gong, R., Liu, X., Bai, X., Song, J., Sebe, N.: Binary neural networks: A survey. Pattern Recognition 105, 107281 (2020). https:\/\/doi.org\/10.1016\/j.patcog.2020.107281, https:\/\/www.sciencedirect.com\/science\/article\/pii\/S0031320320300856","DOI":"10.1016\/j.patcog.2020.107281"},{"key":"9_CR104","doi-asserted-by":"crossref","unstructured":"S\u00e4lzer, M., Lange, M.: Reachability Is NP-Complete Even for the Simplest Neural Networks. In: Proc. 15th Int. Conf. on Reachability Problems (RP). pp. 149\u2013164 (2021)","DOI":"10.1007\/978-3-030-89716-1_10"},{"key":"9_CR105","unstructured":"Schl\u00f6gl, A., Hofer, N., B\u00f6hme, R.: Causes and effects of unanticipated numerical deviations in neural network inference frameworks. In: Oh, A., Naumann, T., Globerson, A., Saenko, K., Hardt, M., Levine, S. (eds.) Advances in Neural Information Processing Systems. vol.\u00a036, pp. 56095\u201356107. Curran Associates, Inc. (2023), https:\/\/proceedings.neurips.cc\/paper_files\/paper\/2023\/file\/af076c3bdbf935b81d808e37c5ede463-Paper-Conference.pdf"},{"key":"9_CR106","doi-asserted-by":"publisher","unstructured":"Seshia, S.A., Sadigh, D., Sastry, S.S.: Toward verified artificial intelligence. Commun. ACM 65(7), 46\u201355 (Jun 2022). https:\/\/doi.org\/10.1145\/3503914","DOI":"10.1145\/3503914"},{"key":"9_CR107","doi-asserted-by":"crossref","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)","DOI":"10.1007\/978-3-030-81685-8_6"},{"key":"9_CR108","doi-asserted-by":"publisher","unstructured":"Sibidanov, A., Zimmermann, P., Glondu, S.: The core-math project. In: 2022 IEEE 29th Symposium on Computer Arithmetic (ARITH). pp. 26\u201334 (2022). https:\/\/doi.org\/10.1109\/ARITH54963.2022.00014","DOI":"10.1109\/ARITH54963.2022.00014"},{"key":"9_CR109","unstructured":"Sidrane, C., Kochenderfer, M.J.: OVERT: Verification of nonlinear dynamical systems with neural network controllers via overapproximation. Safe Machine Learning workshop at ICLR (2019)"},{"key":"9_CR110","doi-asserted-by":"crossref","unstructured":"Singh, G., Gehr, T., P\u00fcschel, M., Vechev, M.: An abstract domain for certifying neural networks. Proceedings of the ACM on Programming Languages 3(POPL), 1\u201330 (2019)","DOI":"10.1145\/3290354"},{"key":"9_CR111","doi-asserted-by":"publisher","unstructured":"Slusarz, N., Komendantskaya, E., Daggitt, M.L., Stewart, R.J., Stark, K.: Logic of differentiable logics: Towards a uniform semantics of DL. In: Piskac, R., Voronkov, A. (eds.) LPAR 2023: Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Manizales, Colombia, 4-9th June 2023. EPiC Series in Computing, vol.\u00a094, pp. 473\u2013493. EasyChair (2023). https:\/\/doi.org\/10.29007\/C1NT, https:\/\/doi.org\/10.29007\/c1nt","DOI":"10.29007\/C1NT 10.29007\/c1nt"},{"key":"9_CR112","unstructured":"Szegedy, C., Zaremba, W., Sutskever, I., Bruna, J., Erhan, D., Goodfellow, I., Fergus, R.: Intriguing properties of neural networks (2014)"},{"key":"9_CR113","doi-asserted-by":"publisher","unstructured":"Tassarotti, J., Tristan, J.B.: Verified density compilation for a probabilistic programming language. Proc. ACM Program. Lang. 7(PLDI) (Jun 2023). https:\/\/doi.org\/10.1145\/3591245, https:\/\/doi.org\/10.1145\/3591245","DOI":"10.1145\/3591245 10.1145\/3591245"},{"key":"9_CR114","doi-asserted-by":"publisher","unstructured":"Teuber, S., B\u00fcning, M.K., Kern, P., Sinz, C.: Geometric path enumeration for equivalence verification of neural networks. In: 2021 IEEE 33rd International Conference on Tools with Artificial Intelligence (ICTAI). pp. 200\u2013208 (2021). https:\/\/doi.org\/10.1109\/ICTAI52525.2021.00035","DOI":"10.1109\/ICTAI52525.2021.00035"},{"key":"9_CR115","doi-asserted-by":"publisher","unstructured":"Teuber, S., Mitsch, S., Platzer, A.: Provably safe neural network controllers via differential dynamic logic. CoRR abs\/2402.10998 (2024). https:\/\/doi.org\/10.48550\/ARXIV.2402.10998, https:\/\/doi.org\/10.48550\/arXiv.2402.10998","DOI":"10.48550\/ARXIV.2402.10998 10.48550\/arXiv.2402.10998"},{"key":"9_CR116","doi-asserted-by":"publisher","unstructured":"Tran, H.D., Xiang, W., Johnson, T.T.: Verification approaches for learning-enabled autonomous cyber\u2013physical systems. IEEE Design & Test 39(1), 24\u201334 (2022). https:\/\/doi.org\/10.1109\/MDAT.2020.3015712","DOI":"10.1109\/MDAT.2020.3015712"},{"key":"9_CR117","doi-asserted-by":"crossref","unstructured":"Tran, H.D., Yang, X., Lopez, D.M., Musau, P., Nguyen, L.V., Xiang, W., Bak, S., Johnson, T.T.: NNV: The neural network verification tool for deep neural networks and learning-enabled cyber-physical systems. In: 32nd International Conference on Computer-Aided Verification (CAV\u201920) (7 2020)","DOI":"10.1007\/978-3-030-53288-8_1"},{"key":"9_CR118","unstructured":"Wang, N., Choi, J., Brand, D., Chen, C.Y., Gopalakrishnan, K.: Training deep neural networks with 8-bit floating point numbers. 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\/335d3d1cd7ef05ec77714a215134914c-Paper.pdf"},{"key":"9_CR119","unstructured":"Wang, S., Zhang, H., Xu, K., Lin, X., Jana, S., Hsieh, C.J., Kolter, J.Z.: Beta-crown: Efficient bound propagation with per-neuron split constraints for neural network robustness verification. Advances in Neural Information Processing Systems 34, 29909\u201329921 (2021)"},{"key":"9_CR120","doi-asserted-by":"crossref","unstructured":"Wu, H., Isac, O., Zeljic, A., Tagomori, T., Daggitt, M.L., Kokke, W., Refaeli, I., Amir, G., Julian, K., Bassan, S., Huang, P., Lahav, O., Wu, M., Zhang, M., Komendantskaya, E., Katz, G., Barrett, C.W.: Marabou 2.0: A Versatile Formal Analyzer of Neural Networks. In: Computer Aided Verification (CAV) (2024)","DOI":"10.1007\/978-3-031-65630-9_13"},{"key":"9_CR121","doi-asserted-by":"crossref","unstructured":"Wu, H., Zelji\u0107, A., Katz, G., Barrett, C.: Efficient neural network analysis with sum-of-infeasibilities. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems. pp. 143\u2013163. Springer (2022)","DOI":"10.1007\/978-3-030-99524-9_8"},{"key":"9_CR122","doi-asserted-by":"crossref","unstructured":"Xiang, W., Tran, H.D., Johnson, T.T.: Output reachable set estimation and verification for multilayer neural networks. IEEE transactions on neural networks and learning systems 29(11), 5777\u20135783 (2018)","DOI":"10.1109\/TNNLS.2018.2808470"},{"key":"9_CR123","doi-asserted-by":"publisher","unstructured":"Xie, X., Kersting, K., Neider, D.: Neuro-symbolic verification of deep neural networks. In: Raedt, L.D. (ed.) Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence, IJCAI-22. pp. 3622\u20133628. International Joint Conferences on Artificial Intelligence Organization (7 2022). https:\/\/doi.org\/10.24963\/ijcai.2022\/503, https:\/\/doi.org\/10.24963\/ijcai.2022\/503, main Track","DOI":"10.24963\/ijcai.2022\/503 10.24963\/ijcai.2022\/503"},{"key":"9_CR124","doi-asserted-by":"crossref","unstructured":"Yao, P., Wu, H., Gao, B., Tang, J., Zhang, Q., Zhang, W., Yang, J.J., Qian, H.: Fully hardware-implemented memristor convolutional neural network. Nature 577(7792), 641\u2013646 (2020)","DOI":"10.1038\/s41586-020-1942-4"},{"key":"9_CR125","unstructured":"Zhang, H., Chen, H., Xiao, C., Gowal, S., Stanforth, R., Li, B., Boning, D., Hsieh, C.J.: Towards stable and efficient training of verifiably robust neural networks. In: 8th International Conference on Learning Representations, ICLR 2020 (2020)"},{"key":"9_CR126","doi-asserted-by":"crossref","unstructured":"Zhang, Y., Song, F., Sun, J.: Qebverif: Quantization error bound verification of neural networks. In: Enea, C., Lal, A. (eds.) Computer Aided Verification. pp. 413\u2013437. Springer Nature Switzerland, Cham (2023)","DOI":"10.1007\/978-3-031-37703-7_20"},{"key":"9_CR127","unstructured":"Zhang, Y., Albarghouthi, A., D\u2019Antoni, L.: Robustness to programmable string transformations via augmented abstract training. In: Proceedings of the 37th International Conference on Machine Learning. pp. 11023\u201311032 (2020)"},{"key":"9_CR128","unstructured":"Zhuang, D., Zhang, X., Song, S., Hooker, S.: Randomness in neural network training: Characterizing the impact of tooling. In: Marculescu, D., Chi, Y., Wu, C. (eds.) Proceedings of Machine Learning and Systems. vol.\u00a04, pp. 316\u2013336 (2022), https:\/\/proceedings.mlsys.org\/paper_files\/paper\/2022\/file\/427e0e886ebf87538afdf0badb805b7f-Paper.pdf"},{"key":"9_CR129","unstructured":"Zombori, D., B\u00e1nhelyi, B., Csendes, T., Megyeri, I., Jelasity, M.: Fooling a complete neural network verifier. In: International Conference on Learning Representations (2021), https:\/\/openreview.net\/forum?id=4IwieFS44l"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-91118-7_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T08:18:30Z","timestamp":1746001110000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-91118-7_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031911170","9783031911187"],"references-count":129,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-91118-7_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"1 May 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ESOP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"European Symposium on Programming","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Hamilton, ON","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 May 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 May 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"34","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2025\/conferences\/esop\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}