{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,17]],"date-time":"2026-07-17T22:43:36Z","timestamp":1784328216138,"version":"3.55.0"},"publisher-location":"Cham","reference-count":67,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032071057","type":"print"},{"value":"9783032071064","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,10,6]],"date-time":"2025-10-06T00:00:00Z","timestamp":1759708800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,10,6]],"date-time":"2025-10-06T00:00:00Z","timestamp":1759708800000},"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":[[2026]]},"DOI":"10.1007\/978-3-032-07106-4_2","type":"book-chapter","created":{"date-parts":[[2025,10,7]],"date-time":"2025-10-07T14:38:04Z","timestamp":1759847884000},"page":"11-33","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Verifying Neural Networks with\u00a0PyRAT"],"prefix":"10.1007","author":[{"given":"Augustin","family":"Lemesle","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Julien","family":"Lehmann","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Tristan Le","family":"Gall","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Zakaria","family":"Chihani","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2025,10,6]]},"reference":[{"key":"2_CR1","doi-asserted-by":"crossref","unstructured":"Bak, S.: nnenum: Verification of relu neural networks with optimized abstraction refinement. In: NASA Formal Methods Symposium. pp. 19\u201336. Springer (2021)","DOI":"10.1007\/978-3-030-76384-8_2"},{"key":"2_CR2","doi-asserted-by":"crossref","unstructured":"Bak, S., Tran, H.D., Hobbs, K., Johnson, T.T.: Improved geometric path enumeration for verifying ReLU neural networks. In: 32nd International Conference on Computer-Aided Verification (CAV) (July 2020)","DOI":"10.1007\/978-3-030-53288-8_4"},{"key":"2_CR3","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org (2016)"},{"key":"2_CR4","doi-asserted-by":"publisher","DOI":"10.1016\/j.automatica.2023.111107","volume":"154","author":"TJ Bird","year":"2023","unstructured":"Bird, T.J., Pangborn, H.C., Jain, N., Koeln, J.P.: Hybrid zonotopes: A new set representation for reachability analysis of mixed logical dynamical systems. Automatica 154, 111107 (2023)","journal-title":"Automatica"},{"key":"2_CR5","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":"2_CR6","doi-asserted-by":"crossref","unstructured":"Brix, C., Bak, S., Liu, C., Johnson, T.T.: The fourth international verification of neural networks competition (vnn-comp 2023): Summary and results. arXiv preprint arXiv:2312.16760 (2023)","DOI":"10.1007\/s10009-023-00703-4"},{"issue":"42","key":"2_CR7","first-page":"1","volume":"21","author":"R Bunel","year":"2020","unstructured":"Bunel, R., Lu, J., Turkaslan, I., Torr, P.H., Kohli, P., Kumar, M.P.: Branch and bound for piecewise linear neural network verification. J. Mach. Learn. Res. 21(42), 1\u201339 (2020)","journal-title":"J. Mach. Learn. Res."},{"key":"2_CR8","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-540-89330-1_2","volume-title":"Programming Languages and Systems","author":"L Chen","year":"2008","unstructured":"Chen, L., Min\u00e9, A., Cousot, P.: A sound floating-point polyhedra abstract domain. In: Ramalingam, G. (ed.) Programming Languages and Systems, pp. 3\u201318. Springer, Berlin Heidelberg, Berlin, Heidelberg (2008)"},{"key":"2_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Logics of Programs","author":"EM Clarke","year":"1982","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52\u201371. Springer, Heidelberg (1982). https:\/\/doi.org\/10.1007\/BFb0025774"},{"key":"2_CR10","doi-asserted-by":"publisher","unstructured":"Clarke, E.M., Emerson, E.A., Sifakis, J.: Model checking: algorithmic verification and debugging. Commun. ACM 52(11), 74\u201384 (Nov 2009). https:\/\/doi.org\/10.1145\/1592761.1592781, https:\/\/doi.org\/10.1145\/1592761.1592781","DOI":"10.1145\/1592761.1592781"},{"key":"2_CR11","unstructured":"Comba, J.L.D., Stol, J.: Affine arithmetic and its applications to computer graphics. In: Proceedings of VI SIBGRAPI (Brazilian Symposium on Computer Graphics and Image Processing). pp. 9\u201318 (1993)"},{"key":"2_CR12","unstructured":"Confiance.ai: Benchmark for abstract interpretation training (Mar 2024)"},{"key":"2_CR13","unstructured":"Cousot, P.: Principles of Abstract Interpretation. MIT Press (2022)"},{"key":"2_CR14","doi-asserted-by":"crossref","unstructured":"Cousot, Patrick, 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 \u201977 (1977)","DOI":"10.1145\/512950.512973"},{"key":"2_CR15","doi-asserted-by":"publisher","unstructured":"Damour, M., de\u00a0Grancey, F., Gabreau, C., Gauffriau, A., Ginestet, J.B., Hervieu, A., Huraux, T., Pagetti, C., Ponsolle, L., Clavi\u00e8re, A.: Towards Certification of a Reduced Footprint ACAS-Xu System: a Hybrid ML-based Solution. In: SAFECOMP 2021: Computer Safety, Reliability, and Security. pp. 34\u201348 (Aug 2021). https:\/\/doi.org\/10.1007\/978-3-030-83903-1_3, https:\/\/hal.science\/hal-03355299","DOI":"10.1007\/978-3-030-83903-1_3"},{"key":"2_CR16","unstructured":"Dawood, H.: Theories of interval arithmetic: mathematical foundations and applications. LAP Lambert Academic Publishing (2011)"},{"key":"2_CR17","doi-asserted-by":"publisher","unstructured":"Duong, H., Xu, D., Nguyen, T., Dwyer, M.B.: Harnessing neuron stability to improve DNN verification. Proc. ACM Softw. Eng. 1(FSE), 859\u2013881 (2024). https:\/\/doi.org\/10.1145\/3643765, https:\/\/doi.org\/10.1145\/3643765","DOI":"10.1145\/3643765"},{"key":"2_CR18","unstructured":"Durand, S., Lemesle, A., Chihani, Z., Urban, C., Terrier, F.: Reciph: Relational coefficients for input partitioning heuristic. In: 1st Workshop on Formal Verification of Machine Learning (WFVML 2022) (2022)"},{"key":"2_CR19","doi-asserted-by":"crossref","unstructured":"Dutta, S., Jha, S., Sanakaranarayanan, S., Tiwari, A.: Output range analysis for deep neural networks. arXiv preprint arXiv:1709.09130 (2017)","DOI":"10.1007\/978-3-319-77935-5_9"},{"key":"2_CR20","unstructured":"Ferrari, C., Muller, M.N., Jovanovic, N., Vechev, M.: Complete verification via multi-neuron relaxation guided branch-and-bound. arXiv preprint arXiv:2205.00263 (2022)"},{"key":"2_CR21","unstructured":"Gabreau, C., Teuli\u00e8res, M.C., Jenn, E., Lemesle, A., Potop-Butucaru, D., Thiant, F., Fischer, L., Turki, M.: A study of an ACAS-Xu exact implementation using ED-324\/ARP6983. In: 12th European Congress Embedded Real Time Systems - ERTS 2024. Toulouse (31000), France (Jun 2024), https:\/\/hal.science\/hal-04584782"},{"key":"2_CR22","doi-asserted-by":"crossref","unstructured":"Gehr, T., Mirman, M., Drachsler-Cohen, D., Tsankov, P., Chaudhuri, S., Vechev, M.: Ai2: Safety and robustness certification of neural networks with abstract interpretation. In: 2018 IEEE symposium on security and privacy (SP). pp. 3\u201318. IEEE (2018)","DOI":"10.1109\/SP.2018.00058"},{"key":"2_CR23","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.science\/hal-03687211"},{"key":"2_CR24","doi-asserted-by":"crossref","unstructured":"Glunt, J.J., Robbins, J.A., Silvestre, D., Pangborn, H.C.: Sharp hybrid zonotopes: Set operations and the reformulation-linearization technique (2025), https:\/\/arxiv.org\/abs\/2503.17483","DOI":"10.1109\/LCSYS.2025.3585953"},{"key":"2_CR25","unstructured":"Goodfellow, I.J., Shlens, J., Szegedy, C.: Explaining and harnessing adversarial examples (2015), https:\/\/arxiv.org\/abs\/1412.6572"},{"key":"2_CR26","doi-asserted-by":"publisher","unstructured":"Goubault, E.: Static analyses of the precision of floating-point operations. In: Cousot, P. (ed.) Static Analysis, 8th International Symposium, SAS 2001, Paris, France, July 16-18, 2001, Proceedings. Lecture Notes in Computer Science, vol.\u00a02126, pp. 234\u2013259. Springer (2001). https:\/\/doi.org\/10.1007\/3-540-47764-0_14, https:\/\/doi.org\/10.1007\/3-540-47764-0_14","DOI":"10.1007\/3-540-47764-0_14"},{"key":"2_CR27","unstructured":"Goubault, E., Putot, S.: A zonotopic framework for functional abstractions (2009), https:\/\/arxiv.org\/abs\/0910.1763"},{"key":"2_CR28","doi-asserted-by":"publisher","unstructured":"Harris, C.R., Millman, K.J., van\u00a0der Walt, S.J., Gommers, R., Virtanen, P., Cournapeau, D., Wieser, E., Taylor, J., Berg, S., Smith, N.J., Kern, R., Picus, M., Hoyer, S., van Kerkwijk, M.H., Brett, M., Haldane, A., del R\u00edo, J.F., Wiebe, M., Peterson, P., G\u00e9rard-Marchant, P., Sheppard, K., Reddy, T., Weckesser, W., Abbasi, H., Gohlke, C., Oliphant, T.E.: Array programming with NumPy. Nature 585(7825), 357\u2013362 (Sep 2020). https:\/\/doi.org\/10.1038\/s41586-020-2649-2, https:\/\/doi.org\/10.1038\/s41586-020-2649-2","DOI":"10.1038\/s41586-020-2649-2"},{"key":"2_CR29","doi-asserted-by":"publisher","unstructured":"Hickey, T., Ju, Q., Van\u00a0Emden, M.H.: Interval arithmetic: From principles to implementation. J. ACM 48(5), 1038\u20131068 (sep 2001). https:\/\/doi.org\/10.1145\/502102.502106, https:\/\/doi.org\/10.1145\/502102.502106","DOI":"10.1145\/502102.502106"},{"key":"2_CR30","series-title":"Lecture Notes in Computer Science","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.) CAV 2017. LNCS, vol. 10426, pp. 3\u201329. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_1"},{"key":"2_CR31","doi-asserted-by":"publisher","unstructured":"Jeannet, B., Min\u00e9, A.: Apron: A library of numerical abstract domains for static analysis. In: Bouajjani, A., Maler, O. (eds.) Computer Aided Verification, 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings. Lecture Notes in Computer Science, vol.\u00a05643, pp. 661\u2013667. Springer (2009). https:\/\/doi.org\/10.1007\/978-3-642-02658-4_52, https:\/\/doi.org\/10.1007\/978-3-642-02658-4_52","DOI":"10.1007\/978-3-642-02658-4_52"},{"key":"2_CR32","volume-title":"An algorithm to reduce the number of dummy variables in affine arithmetic","author":"M Kashiwagi","year":"2012","unstructured":"Kashiwagi, M.: An algorithm to reduce the number of dummy variables in affine arithmetic. Scientific Computing, Computer Arithmetic and Verified Numerical Computations (SCAN) (2012)"},{"key":"2_CR33","doi-asserted-by":"crossref","unstructured":"Katz, G., Barrett, C., Dill, D., Julian, K., Kochenderfer, M.: Reluplex: An efficient smt solver for verifying deep neural networks (2017), https:\/\/arxiv.org\/abs\/1702.01135","DOI":"10.1007\/978-3-319-63387-9_5"},{"key":"2_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/978-3-319-63387-9_5","volume-title":"Computer Aided Verification","author":"G Katz","year":"2017","unstructured":"Katz, G., Barrett, C., Dill, D.L., Julian, K., Kochenderfer, M.J.: Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 97\u2013117. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_5"},{"key":"2_CR35","doi-asserted-by":"publisher","unstructured":"Kochdumper, N., Schilling, C., Althoff, M., Bak, S.: Open- and closed-loop neural network verification using polynomial zonotopes. In: Rozier, K.Y., Chaudhuri, S. (eds.) NASA Formal Methods - 15th International Symposium, NFM 2023, Houston, TX, USA, May 16-18, 2023, Proceedings. Lecture Notes in Computer Science, vol. 13903, pp. 16\u201336. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-33170-1_2, https:\/\/doi.org\/10.1007\/978-3-031-33170-1_2","DOI":"10.1007\/978-3-031-33170-1_2"},{"key":"2_CR36","doi-asserted-by":"publisher","unstructured":"Kochdumper, N., Schilling, C., Althoff, M., Bak, S.: Open- and Closed-Loop Neural Network Verification Using Polynomial Zonotopes, p. 16\u201336. Springer Nature Switzerland (2023). https:\/\/doi.org\/10.1007\/978-3-031-33170-1_2, http:\/\/dx.doi.org\/10.1007\/978-3-031-33170-1_2","DOI":"10.1007\/978-3-031-33170-1_2"},{"key":"2_CR37","unstructured":"Lemesle, A., Lehmann, J., Gall, T.L.: Neural network verification with pyrat (2024), https:\/\/arxiv.org\/abs\/2410.23903"},{"key":"2_CR38","doi-asserted-by":"publisher","first-page":"296","DOI":"10.1007\/978-3-030-32304-2_15","volume-title":"Static Analysis","author":"J Li","year":"2019","unstructured":"Li, J., Liu, J., Yang, P., Chen, L., Huang, X., Zhang, L.: Analyzing deep neural networks with symbolic propagation: Towards higher precision and faster verification. In: Chang, B.Y.E. (ed.) Static Analysis, pp. 296\u2013319. Springer International Publishing, Cham (2019)"},{"key":"2_CR39","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: 35th International Conference on Computer-Aided Verification (CAV) (July 2023)","DOI":"10.1007\/978-3-031-37703-7_19"},{"key":"2_CR40","unstructured":"Madry, A., Makelov, A., Schmidt, L., Tsipras, D., Vladu, A.: Towards deep learning models resistant to adversarial attacks (2019), https:\/\/arxiv.org\/abs\/1706.06083"},{"key":"2_CR41","doi-asserted-by":"crossref","unstructured":"Manfredi, G., Jestin, Y.: An Introduction to ACAS Xu and the Challenges Ahead. In: DASC, 2016 IEEE\/AIAA 35th Digital Avionics Systems Conference. pp. .ISBN: 978\u20131\u20135090\u20132524\u20134. Digital Avionics Systems Conference (DASC), 2016 IEEE\/AIAA 35th, Sacramento, United States (Sep 2016), https:\/\/enac.hal.science\/hal-01638049","DOI":"10.1109\/DASC.2016.7778055"},{"key":"2_CR42","doi-asserted-by":"publisher","first-page":"308","DOI":"10.1007\/978-3-030-88806-0_15","volume-title":"Static Analysis","author":"D Mazzucato","year":"2021","unstructured":"Mazzucato, D., Urban, C.: Reduced products of abstract domains for fairness certification of neural networks. In: Dr\u0103goi, C., Mukherjee, S., Namjoshi, K. (eds.) Static Analysis, pp. 308\u2013322. Springer International Publishing, Cham (2021)"},{"key":"2_CR43","unstructured":"Mirman, M., Singh, G., Vechev, M.: A provable defense for deep residual networks (2020), https:\/\/arxiv.org\/abs\/1903.12519"},{"key":"2_CR44","unstructured":"Moore, R.E.: Interval analysis, vol.\u00a04. prentice-Hall Englewood Cliffs (1966)"},{"key":"2_CR45","doi-asserted-by":"crossref","unstructured":"Moosavi-Dezfooli, S.M., Fawzi, A., Frossard, P.: Deepfool: a simple and accurate method to fool deep neural networks (2016), https:\/\/arxiv.org\/abs\/1511.04599","DOI":"10.1109\/CVPR.2016.282"},{"key":"2_CR46","doi-asserted-by":"crossref","unstructured":"Ortiz, J., Vellucci, A., Koeln, J., Ruths, J.: Hybrid zonotopes exactly represent relu neural networks. In: 2023 62nd IEEE Conference on Decision and Control (CDC). pp. 5351\u20135357. IEEE (2023)","DOI":"10.1109\/CDC49753.2023.10383944"},{"key":"2_CR47","unstructured":"Paszke, A., Gross, S., Massa, F., Lerer, A., Bradbury, J., Chanan, G., Killeen, T., Lin, Z., Gimelshein, N., Antiga, L., Desmaison, A., K\u00f6pf, A., Yang, E., DeVito, Z., Raison, M., Tejani, A., Chilamkurthy, S., Steiner, B., Fang, L., Bai, J., Chintala, S.: Pytorch: An imperative style, high-performance deep learning library (2019), https:\/\/arxiv.org\/abs\/1912.01703"},{"key":"2_CR48","doi-asserted-by":"publisher","unstructured":"Pedrouzo-Ulloa, A., Ramon, J., P\u00e9erez-Gonz\u00e1lez, F., Lilova, S., Duflot, P., Chihani, Z., Gentili, N., Ulivi, P., Hoque, M.A., Mukammel, T., Pritzker, Z., Lemesle, A., Loureiro-Acu\u00f1a, J., Mart\u00ednez, X., Jim\u00e9nez-Balsa, G.: Introducing the trumpet project: Trustworthy multi-site privacy enhancing technologies. In: 2023 IEEE International Conference on Cyber Security and Resilience (CSR). pp. 604\u2013611 (2023).https:\/\/doi.org\/10.1109\/CSR57506.2023.10224961","DOI":"10.1109\/CSR57506.2023.10224961"},{"issue":"2","key":"2_CR49","doi-asserted-by":"publisher","first-page":"117","DOI":"10.3233\/AIC-2012-0525","volume":"25","author":"L Pulina","year":"2012","unstructured":"Pulina, L., Tacchella, A.: Challenging smt solvers to verify neural networks. AI Commun. 25(2), 117\u2013135 (2012)","journal-title":"AI Commun."},{"key":"2_CR50","doi-asserted-by":"publisher","unstructured":"Scott, J.K., Raimondo, D.M., Marseglia, G.R., Braatz, R.D.: Constrained zonotopes: A new tool for set-based estimation and fault detection. Automatica 69, 126\u2013136 (Jul 2016). https:\/\/doi.org\/10.1016\/j.automatica.2016.02.036, https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0005109816300772","DOI":"10.1016\/j.automatica.2016.02.036"},{"key":"2_CR51","doi-asserted-by":"publisher","unstructured":"Shriver, D., Elbaum, S., Dwyer, M.B.: DNNV: A Framework for Deep Neural Network Verification, p. 137\u2013150. Springer International Publishing (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_6, http:\/\/dx.doi.org\/10.1007\/978-3-030-81685-8_6","DOI":"10.1007\/978-3-030-81685-8_6"},{"key":"2_CR52","doi-asserted-by":"publisher","unstructured":"Sidarta, D.E., O\u2019Sullivan, J., Lim, H.J.: Damage Detection of Offshore Platform Mooring Line Using Artificial Neural Network. In: International Conference on Offshore Mechanics and Arctic Engineering. vol. Volume 1: Offshore Technology, p. V001T01A058 (06 2018).https:\/\/doi.org\/10.1115\/OMAE2018-77084, https:\/\/doi.org\/10.1115\/OMAE2018-77084","DOI":"10.1115\/OMAE2018-77084"},{"key":"2_CR53","unstructured":"Singh, G., Gehr, T., Mirman, M., P\u00fcschel, M., Vechev, M.: Fast and effective robustness certification. In: Proceedings of the 32nd International Conference on Neural Information Processing Systems. p. 10825\u201310836. NIPS\u201918, Curran Associates Inc., Red Hook, NY, USA (2018)"},{"key":"2_CR54","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":"2_CR55","unstructured":"Tjeng, V., Xiao, K., Tedrake, R.: Evaluating robustness of neural networks with mixed integer programming. arXiv preprint arXiv:1711.07356 (2017)"},{"key":"2_CR56","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) (July 2020)","DOI":"10.1007\/978-3-030-53288-8_1"},{"key":"2_CR57","doi-asserted-by":"publisher","unstructured":"Uewichitrapochana, P., Surarerks, A.: Signed-symmetric function approximation in affine arithmetic. In: 2013 10th International Conference on Electrical Engineering\/Electronics, Computer, Telecommunications and Information Technology. pp.\u00a01\u20136 (05 2013). https:\/\/doi.org\/10.1109\/ECTICon.2013.6559630","DOI":"10.1109\/ECTICon.2013.6559630"},{"key":"2_CR58","doi-asserted-by":"publisher","unstructured":"Urban, C., Christakis, M., W\u00fcstholz, V., Zhang, F.: Perfectly parallel fairness certification of neural networks. Proc. ACM Program. Lang. 4(OOPSLA) (Nov 2020). https:\/\/doi.org\/10.1145\/3428253, https:\/\/doi.org\/10.1145\/3428253","DOI":"10.1145\/3428253"},{"key":"2_CR59","unstructured":"Urban, C., Min\u00e9, A.: A review of formal methods applied to machine learning (2021), https:\/\/arxiv.org\/abs\/2104.02466"},{"key":"2_CR60","unstructured":"Wang, S., Pei, K., Whitehouse, J., Yang, J., Jana, S.: Formal security analysis of neural networks using symbolic intervals. In: 27th USENIX Security Symposium (USENIX Security 18). pp. 1599\u20131614 (2018)"},{"key":"2_CR61","unstructured":"Wang, S., Zhang, H., Xu, K., Lin, X., Jana, S., Hsieh, C.J., Kolter, Z.: Beta-CROWN: Efficient bound propagation with per-neuron split constraints for complete and incomplete neural network verification. arXiv preprint arXiv:2103.06624 (2021)"},{"key":"2_CR62","unstructured":"Weng, L., Zhang, H., Chen, H., Song, Z., Hsieh, C.J., Daniel, L., Boning, D., Dhillon, I.: Towards fast computation of certified robustness for relu networks. In: International Conference on Machine Learning. pp. 5276\u20135285. PMLR (2018)"},{"key":"2_CR63","unstructured":"Xu, K., Zhang, H., Wang, S., Wang, Y., Jana, S., Lin, X., Hsieh, C.J.: Fast and Complete: Enabling complete neural network verification with rapid and massively parallel incomplete verifiers. In: International Conference on Learning Representations (2021), https:\/\/openreview.net\/forum?id=nVZtXBI6LNn"},{"key":"2_CR64","doi-asserted-by":"publisher","unstructured":"Yin, B., Chen, L., Liu, J., Wang, J.: Efficient complete verification of neural networks via layerwised splitting and refinement. Trans. Comp.-Aided Des. Integ. Cir. Sys. 41(11), 3898\u20133909 (Nov 2022). https:\/\/doi.org\/10.1109\/TCAD.2022.3197534, https:\/\/doi.org\/10.1109\/TCAD.2022.3197534","DOI":"10.1109\/TCAD.2022.3197534"},{"key":"2_CR65","unstructured":"Zhang, H., Weng, T.W., Chen, P.Y., Hsieh, C.J., Daniel, L.: Efficient neural network robustness certification with general activation functions. Advances in Neural Information Processing Systems 31, 4939\u20134948 (2018), https:\/\/arxiv.org\/pdf\/1811.00866.pdf"},{"key":"2_CR66","doi-asserted-by":"crossref","unstructured":"Zhang, Y., Zhang, H., Xu, X.: Backward reachability analysis of neural feedback systems using hybrid zonotopes. IEEE Control Systems Letters (2023)","DOI":"10.1109\/LCSYS.2023.3289572"},{"key":"2_CR67","unstructured":"Zhou, X., Xu, H., Xu, A., Shi, Z., Hsieh, C.J., Zhang, H.: Testing neural network verifiers: A soundness benchmark with hidden counterexamples (2024), https:\/\/arxiv.org\/abs\/2412.03154"}],"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-032-07106-4_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T22:04:06Z","timestamp":1760047446000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-07106-4_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,6]]},"ISBN":["9783032071057","9783032071064"],"references-count":67,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-07106-4_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,10,6]]},"assertion":[{"value":"6 October 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"(current) Augustin Lemesle, Julien Lehmann, Tristan Le Gall; (past) Serge Durand, Samuel Akinwande.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Main Contributors"}},{"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":"Singapore","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Singapore","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":"13 October 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14 October 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sas2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/2025.splashcon.org\/home\/sas-2025","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}