{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,13]],"date-time":"2026-01-13T18:48:24Z","timestamp":1768330104799,"version":"3.49.0"},"publisher-location":"Cham","reference-count":74,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032156990","type":"print"},{"value":"9783032157003","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"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-15700-3_6","type":"book-chapter","created":{"date-parts":[[2026,1,13]],"date-time":"2026-01-13T12:30:20Z","timestamp":1768307420000},"page":"99-124","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Proof Minimization in\u00a0Neural Network Verification"],"prefix":"10.1007","author":[{"given":"Omri","family":"Isac","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Idan","family":"Refaeli","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Haoze","family":"Wu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Clark","family":"Barrett","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Guy","family":"Katz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2026,1,13]]},"reference":[{"key":"6_CR1","doi-asserted-by":"crossref","unstructured":"Abraham, E., Kremer, G.: SMT solving for arithmetic theories: theory and tool support. In: Proceedings of the 19th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC), pp.\u00a01\u20138 (2017)","DOI":"10.1109\/SYNASC.2017.00009"},{"key":"6_CR2","doi-asserted-by":"crossref","unstructured":"Akintunde, M., Kevorchian, A., Lomuscio, A., Pirovano, E.: Verification of RNN-based neural agent-environment systems. In: Proceedings of the 33rd AAAI Conference on Artificial Intelligence (AAAI), pp. 197\u2013210 (2019)","DOI":"10.1609\/aaai.v33i01.33016006"},{"key":"6_CR3","doi-asserted-by":"crossref","unstructured":"Amir, G., Freund, Z., Katz, G., Mandelbaum, E., Refaeli, I.: veriFIRE: verifying an industrial, learning-based wildfire detection system. In: Proceedings of the 25th International Symposium on Formal Methods (FM), pp. 648\u2013656 (2023)","DOI":"10.1007\/978-3-031-27481-7_38"},{"key":"6_CR4","doi-asserted-by":"crossref","unstructured":"Amir, G., et al.: Verifying learning-based robotic navigation systems. In: Proceedings of the 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp. 607\u2013627 (2023)","DOI":"10.1007\/978-3-031-30823-9_31"},{"key":"6_CR5","doi-asserted-by":"crossref","unstructured":"Avni, G., Bloem, R., Chatterjee, K., Henzinger, T., Konighofer, B., Pranger, S.: Run-time optimization for learned controllers through quantitative games. In: Proceedings of the 31st International Conference on Computer Aided Verification (CAV), pp. 630\u2013649 (2019)","DOI":"10.1007\/978-3-030-25540-4_36"},{"key":"6_CR6","doi-asserted-by":"crossref","unstructured":"Baluta, T., Shen, S., Shinde, S., Meel, K., Saxena, P.: Quantitative verification of neural networks and its security applications. In: Proceedings of the 26th ACM Conference on Computer and Communication Security (CCS) (2019)","DOI":"10.1145\/3319535.3354245"},{"issue":"10","key":"6_CR7","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1145\/3587692","volume":"66","author":"H Barbosa","year":"2023","unstructured":"Barbosa, H., et al.: Generating and Exploiting Automated Reasoning Proof Certificates. Commun. ACM 66(10), 86\u201395 (2023)","journal-title":"Commun. ACM"},{"key":"6_CR8","doi-asserted-by":"crossref","unstructured":"Barrett, C., Tinelli, C.: Satisfiability Modulo Theories. In: Clarke, E., Henzinger, T., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 305\u2013343. Springer International Publishing (2018)","DOI":"10.1007\/978-3-319-10575-8_11"},{"issue":"1","key":"6_CR9","first-page":"23","volume":"55","author":"C Barrett","year":"2015","unstructured":"Barrett, C., de Moura, L., Fontaine, P.: Proofs in satisfiability modulo theories. All about Proofs, Proofs for All 55(1), 23\u201344 (2015)","journal-title":"All about Proofs, Proofs for All"},{"key":"6_CR10","unstructured":"Bayardo\u00a0Jr, R., Schrag, R.: Using CSP look-back techniques to solve real-world SAT Instances. In: Proceedings of the 14th National Conference on Artificial Intelligence (AAAI), pp. 203\u2013208 (1997)"},{"key":"6_CR11","doi-asserted-by":"crossref","unstructured":"Biere, A., Faller, T., Fazekas, K., Fleury, M., Froleyks, N., Pollitt, F.: CaDiCaL 2.0. In: Proceedings of the 36th International Conference on Computer Aided Verification (CAV), pp. 133\u2013152 (2024)","DOI":"10.1007\/978-3-031-65627-9_7"},{"key":"6_CR12","unstructured":"Bojarski, M., et al.: End to end learning for self-driving cars (2016). technical Report. http:\/\/arxiv.org\/abs\/1604.07316"},{"key":"6_CR13","doi-asserted-by":"crossref","unstructured":"Botoeva, E., Kouvaros, P., Kronqvist, J., Lomuscio, A., Misener, R.: Efficient verification of relu-based neural networks via dependency analysis. In: Proceedings of the 34th AAAI Conference on Artificial Intelligence (AAAI), pp. 3291\u20133299 (2020)","DOI":"10.1609\/aaai.v34i04.5729"},{"key":"6_CR14","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1007\/s00165-008-0080-9","volume":"20","author":"A Bradley","year":"2008","unstructured":"Bradley, A., Manna, Z.: Property-directed incremental invariant generation. Formal Aspects Comput. 20, 379\u2013405 (2008)","journal-title":"Formal Aspects Comput."},{"key":"6_CR15","unstructured":"Brix, C., Bak, S., Johnson, T., Wu, H.: The Fifth International Verification of Neural Networks Competition (VNN-COMP 2024): Summary and Results (2024). technical Report. http:\/\/arxiv.org\/abs\/2412.19985"},{"key":"6_CR16","doi-asserted-by":"crossref","unstructured":"Brix, C., M\u00fcller, M., Bak, S., Johnson, T., Liu, C.: First three years of the international verification of neural networks competition (VNN-COMP). Int. J. Softw. Tools Technol. Transfer 1\u201311 (2023)","DOI":"10.1007\/s10009-023-00703-4"},{"key":"6_CR17","doi-asserted-by":"crossref","unstructured":"Casadio, M., et al.: ANTONIO: towards a systematic method of generating NLP benchmarks for verification. In: Proc. 6th Workshop on Formal Methods for ML-Enabled Autonomous Systems (FoMLAS), vol.\u00a016, pp. 59\u201370 (2023)","DOI":"10.29007\/7wxb"},{"key":"6_CR18","doi-asserted-by":"crossref","unstructured":"Casadio, M., et al.: NLP verification: towards a general methodology for certifying robustness. Europ. J. Appl. Math. 1\u201358 (2025)","DOI":"10.1017\/S0956792525000099"},{"key":"6_CR19","doi-asserted-by":"crossref","unstructured":"Cheng, C.H., et al.: Neural networks for safety-critical applications \u2014 challenges, experiments and perspectives. In: Proceedings of the International Conference on Design, Automation and Test in Europe (DATE), pp. 1005\u20131006. IEEE (2018)","DOI":"10.23919\/DATE.2018.8342158"},{"issue":"2","key":"6_CR20","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1287\/ijoc.3.2.157","volume":"3","author":"J Chinneck","year":"1991","unstructured":"Chinneck, J., Dravnieks, E.: Locating minimal infeasible constraint sets in linear programs. ORSA J. Comput. 3(2), 157\u2013168 (1991)","journal-title":"ORSA J. Comput."},{"key":"6_CR21","volume-title":"Linear Programming","author":"V Chv\u00e1tal","year":"1983","unstructured":"Chv\u00e1tal, V.: Linear Programming. W. H, Freeman and Company (1983)"},{"key":"6_CR22","doi-asserted-by":"crossref","unstructured":"Cordeiro, L.C., et al.: Neural Network Verification is a Programming Language Challenge. In: Proceedings of the 34th European Symposium on Programming (ESOP), pp. 206\u2013235 (2025)","DOI":"10.1007\/978-3-031-91118-7_9"},{"issue":"4","key":"6_CR23","doi-asserted-by":"publisher","first-page":"547","DOI":"10.1016\/j.dss.2009.05.016","volume":"47","author":"P Cortez","year":"2009","unstructured":"Cortez, P., Cerdeira, A., Almeida, F., Matos, T., Reis, J.: Modeling Wine Preferences by Data Mining from Physicochemical Properties. Decis. Support Syst. 47(4), 547\u2013553 (2009)","journal-title":"Decis. Support Syst."},{"key":"6_CR24","doi-asserted-by":"crossref","unstructured":"Dantzig, G.: Linear Programming and Extensions. Princeton University Press (1963)","DOI":"10.7249\/R366"},{"key":"6_CR25","unstructured":"Desmartin, R., Isac, O., Komendantskaya, E., Stark, K., Passmore, G., Katz, G.: a certified proof checker for deep neural network verification in imandra. In: Proceedings of the 16th International Conference on Interactive Theorem Proving (ITP), pp. 1\u201321 (2025)"},{"key":"6_CR26","doi-asserted-by":"crossref","unstructured":"Desmartin, R., Isac, O., Passmore, G., Stark, K., Komendantskaya, E., Katz, G.: Towards a certified proof checker for deep neural network verification. In: Proceedings of the 33rd International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR), pp. 198\u2013209 (2023)","DOI":"10.1007\/978-3-031-45784-5_13"},{"key":"6_CR27","doi-asserted-by":"crossref","unstructured":"Dubey, S., Singh, S., Chaudhuri, B.: Activation functions in deep learning: a comprehensive survey and benchmark. Neurocomputing (2022)","DOI":"10.1016\/j.neucom.2022.06.111"},{"key":"6_CR28","unstructured":"Duong, H., Nguyen, T., Dwyer, M.: A DPLL(T) Framework for Verifying Deep Neural Networks (2023), technical Report. http:\/\/arxiv.org\/abs\/2307.10266"},{"key":"6_CR29","doi-asserted-by":"crossref","unstructured":"Ehlers, R.: Formal verification of piece-wise linear feed-forward neural networks. In: Proceedings of the 15th International Symposium on Automated Technology for Verification and Analysis (ATVA), pp. 269\u2013286 (2017)","DOI":"10.1007\/978-3-319-68167-2_19"},{"key":"6_CR30","doi-asserted-by":"crossref","unstructured":"Elboher, Y., et al.: Robustness assessment of a runway object classifier for safe aircraft taxiing. In: Proceedings of the 43rd International Digital Avionics Systems Conference (DASC) (2024)","DOI":"10.1109\/DASC62030.2024.10748680"},{"key":"6_CR31","doi-asserted-by":"crossref","unstructured":"Gehr, T., Mirman, M., Drachsler-Cohen, D., Tsankov, E., Chaudhuri, S., Vechev, M.: AI2: safety and robustness certification of neural networks with abstract interpretation. In: Proceedings of the 39th IEEE Symposium on Security and Privacy (S &P) (2018)","DOI":"10.1109\/SP.2018.00058"},{"key":"6_CR32","unstructured":"Goodfellow, I., Bengio, Y., Courville, A.: Deep Learning. MIT Press (2016)"},{"key":"6_CR33","doi-asserted-by":"crossref","unstructured":"Goubault, E., Palumby, S., Putot, S., Rustenholz, L., Sankaranarayanan, S.: Static analysis of ReLU neural networks with tropical polyhedra. In: Proceedings of the 28th International Static Analysis Symposium (SAS), pp. 166\u2013190 (2021)","DOI":"10.1007\/978-3-030-88806-0_8"},{"key":"6_CR34","unstructured":"The Gurobi Optimizer. https:\/\/www.gurobi.com\/"},{"key":"6_CR35","doi-asserted-by":"crossref","unstructured":"Guthmann, O., Strichman, O., Trostanetski, A.: Minimal unsatisfiable core extraction for SMT. In: In Proceedings 16th International Conference on Formal Methods in Computer-Aided Design (FMCAD), pp. 57\u201364 (2016)","DOI":"10.1109\/FMCAD.2016.7886661"},{"issue":"1","key":"6_CR36","first-page":"1","volume":"55","author":"MJ Heule","year":"2015","unstructured":"Heule, M.J., Biere, A.: Proofs for satisfiability problems. All about Proofs, Proofs for all 55(1), 1\u201322 (2015)","journal-title":"All about Proofs, Proofs for all"},{"key":"6_CR37","doi-asserted-by":"crossref","unstructured":"Huang, X., Kwiatkowska, M., Wang, S., Wu, M.: Safety verification of deep neural networks. In: Proceedings of the 29th International Conference on Computer Aided Verification (CAV), pp. 3\u201329 (2017)","DOI":"10.1007\/978-3-319-63387-9_1"},{"key":"6_CR38","unstructured":"Isac, O., Barrett, C., Zhang, M., Katz, G.: Neural network verification with proof production. In: Proceedings of the 22nd International Conference on Formal Methods in Computer-Aided Design (FMCAD), pp. 38\u201348 (2022)"},{"key":"6_CR39","unstructured":"Isac, O., Zohar, Y., Barrett, C., Katz, G.: DNN verification, reachability, and the exponential function problem. In: Proceedings of the 34th International Conference on Concurrency Theory (CONCUR) (2023)"},{"key":"6_CR40","doi-asserted-by":"crossref","unstructured":"Jia, K., Rinard, M.: Exploiting Verified Neural Networks via Floating Point Numerical Error. In: Proc. 28th Int. Static Analysis Symposium (SAS). pp. 191\u2013205 (2021)","DOI":"10.1007\/978-3-030-88806-0_9"},{"issue":"3","key":"6_CR41","doi-asserted-by":"publisher","first-page":"598","DOI":"10.2514\/1.G003724","volume":"42","author":"K Julian","year":"2019","unstructured":"Julian, K., Kochenderfer, M., Owen, M.: Deep Neural Network Compression for Aircraft Collision Avoidance Systems. J. Guid. Control. Dyn. 42(3), 598\u2013608 (2019)","journal-title":"J. Guid. Control. Dyn."},{"key":"6_CR42","unstructured":"Junker, U.: Quickxplain: conflict detection for arbitrary constraint propagation algorithms. In: Proceedings of the Workshop on Modelling and Solving Problems with Constraints (2001)"},{"key":"6_CR43","unstructured":"Junker, U.: Quickxplain: preferred explanations and relaxations for over-constrained problems. In: Proceedings of the 19th National Conference on Artificial Intelligence (AAAI), pp. 167\u2013172 (2004)"},{"key":"6_CR44","doi-asserted-by":"crossref","unstructured":"Katz, G., Barrett, C., Dill, D., Julian, K., Kochenderfer, M.: Reluplex: a Calculus for Reasoning about Deep Neural Networks. Formal Methods in System Design (FMSD) (2021)","DOI":"10.1007\/s10703-021-00363-7"},{"key":"6_CR45","doi-asserted-by":"crossref","unstructured":"Katz, G., Barrett, C., Tinelli, C., Reynolds, A., Hadarean, L.: Lazy Proofs for DPLL(T)-based SMT solvers. In: Proceedings of the 16th International Conference on Formal Methods in Computer-Aided Design (FMCAD), pp. 93\u2013100 (2016)","DOI":"10.1109\/FMCAD.2016.7886666"},{"key":"6_CR46","doi-asserted-by":"crossref","unstructured":"Katz, G., et al.: The marabou framework for verification and analysis of deep neural networks. In: Proceedings of the 31st International Conference on Computer Aided Verification (CAV), pp. 443\u2013452 (2019)","DOI":"10.1007\/978-3-030-25540-4_26"},{"key":"6_CR47","unstructured":"Koller, L., Ladner, T., Althoff, M.: Set-Based Training for Neural Network Verification (2024), technical Report. http:\/\/arxiv.org\/abs\/2401.14961"},{"key":"6_CR48","doi-asserted-by":"crossref","unstructured":"Kouvaros, P., Leofante, F., Edwards, B., Chung, C., Margineantu, D., Lomuscio, A.: Verification of semantic key point detection for aircraft pose estimation. In: Proceedings of the 20th International Conference on Principles of Knowledge Representation and Reasoning (KR), pp. 757\u2013762 (2023)","DOI":"10.24963\/kr.2023\/77"},{"key":"6_CR49","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10817-007-9084-z","volume":"40","author":"MH Liffiton","year":"2008","unstructured":"Liffiton, M.H., Sakallah, K.A.: Algorithms for computing minimal unsatisfiable subsets of constraints. J. Autom. Reason. 40, 1\u201333 (2008)","journal-title":"J. Autom. Reason."},{"key":"6_CR50","doi-asserted-by":"crossref","unstructured":"Liu, Z., Yang, P., Zhang, L., Huang, X.: DeepCDCL: A CDCL-based neural network verification framework. In: Proceedings of the 18th International Symposium on Theoretical Aspects of Software Engineering (TASE), pp. 343\u2013355 (2024)","DOI":"10.1007\/978-3-031-64626-3_20"},{"key":"6_CR51","doi-asserted-by":"crossref","unstructured":"Lyu, Z., Ko, C.Y., Kong, Z., Wong, N., Lin, D., Daniel, L.: Fastened crown: tightened neural network robustness certificates. In: Proceedings of the 34th AAAI Conference on Artificial Intelligence (AAAI), pp. 5037\u20135044 (2020)","DOI":"10.1609\/aaai.v34i04.5944"},{"issue":"9","key":"6_CR52","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1145\/1995376.1995394","volume":"54","author":"L de Moura","year":"2011","unstructured":"de Moura, L., Bj\u00f8rner, N.: Satisfiability modulo theories: introduction and applications. Commun. ACM 54(9), 69\u201377 (2011)","journal-title":"Commun. ACM"},{"key":"6_CR53","unstructured":"OpenAI: ChatGPT. https:\/\/chatgpt.com"},{"key":"6_CR54","doi-asserted-by":"crossref","unstructured":"Pulina, L., Tacchella, A.: An Abstraction-Refinement Approach to Verification of Artificial Neural Networks. In: Proceedings of the 22nd International Conference on Computer Aided Verification (CAV), pp. 243\u2013257 (2010)","DOI":"10.1007\/978-3-642-14295-6_24"},{"issue":"1","key":"6_CR55","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1038\/s41591-021-01614-0","volume":"28","author":"P Rajpurkar","year":"2022","unstructured":"Rajpurkar, P., Chen, E., Banerjee, O., Topol, E.J.: AI in health and medicine. Nat. Med. 28(1), 31\u201338 (2022)","journal-title":"Nat. Med."},{"key":"6_CR56","doi-asserted-by":"publisher","unstructured":"Refaeli, I., Isac, O.: Proof Minimization in Neural Network Verification (Artifact) (2025). https:\/\/doi.org\/10.5281\/ZENODO.17169557, https:\/\/zenodo.org\/doi\/10.5281\/zenodo.17169557","DOI":"10.5281\/ZENODO.17169557"},{"key":"6_CR57","doi-asserted-by":"crossref","unstructured":"S\u00e4lzer, M., Lange, M.: Reachability Is NP-complete even for the simplest neural networks. In: Proceedings of the 15th International Conference on Reachability Problems (RP), pp. 149\u2013164 (2021)","DOI":"10.1007\/978-3-030-89716-1_10"},{"key":"6_CR58","doi-asserted-by":"crossref","unstructured":"Sankaranarayanan, S., Dutta, S., Mover, S.: Reaching out towards fully verified autonomous systems. In: Proceedings of the 13th International Conference on Reachability Problems (RP), pp. 22\u201332 (2019)","DOI":"10.1007\/978-3-030-30806-3_3"},{"key":"6_CR59","unstructured":"Silva, J., Sakallah, K.: GRASP-a new search algorithm for satisfiability. In: Proceedings of the 15th International Conference on Computer Aided Design (ICCAD), pp. 220\u2013227 (1996)"},{"issue":"5","key":"6_CR60","doi-asserted-by":"publisher","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"JM Silva","year":"1999","unstructured":"Silva, J.M., Sakallah, K.A.: GRASP: a search algorithm for propositional satisfiability. IEEE Trans. Comput. 48(5), 506\u2013521 (1999)","journal-title":"IEEE Trans. Comput."},{"key":"6_CR61","doi-asserted-by":"crossref","unstructured":"Singh, A., Sarita, Y.C., Mendis, C., Singh, G.: Automated verification of soundness of DNN Certifiers. Proc. ACM Programm. Lang. 9 (2025)","DOI":"10.1145\/3720509"},{"key":"6_CR62","doi-asserted-by":"crossref","unstructured":"Singh, G., Gehr, T., Puschel, M., Vechev, M.: An abstract domain for certifying neural networks. In: Proceedings of the 46th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL) (2019)","DOI":"10.1145\/3290354"},{"key":"6_CR63","doi-asserted-by":"crossref","unstructured":"S\u00f6rensson, N., Biere, A.: Minimizing learned clauses. In: Proceedings of the 12th International Conference on Theory and Applications of Satisfiability Testing (SAT), pp. 237\u2013243. Springer (2009)","DOI":"10.1007\/978-3-642-02777-2_23"},{"key":"6_CR64","unstructured":"Szegedy, C., et al.: Intriguing Properties of Neural Networks (2013), technical Report. http:\/\/arxiv.org\/abs\/1312.6199"},{"key":"6_CR65","unstructured":"Tjeng, V., Xiao, K., Tedrake, R.: Evaluating Robustness of Neural Networks with Mixed Integer Programming (2017), technical Report. http:\/\/arxiv.org\/abs\/1711.07356"},{"key":"6_CR66","doi-asserted-by":"crossref","unstructured":"Tran, H.D., Bak, S., Xiang, W., Johnson, T.: Verification of deep convolutional neural networks using imagestars. In: Proceedings of the 32nd International Conference on Computer Aided Verification (CAV), pp. 18\u201342 (2020)","DOI":"10.1007\/978-3-030-53288-8_2"},{"key":"6_CR67","unstructured":"The VNNCOMP 2025 Benchmarks Repository. https:\/\/github.com\/VNN-COMP\/vnncomp2025_benchmarks (2025)"},{"key":"6_CR68","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 Security Symposium, pp. 1599\u20131614 (2018)"},{"key":"6_CR69","unstructured":"Wang, S., et al.: Beta-crown: efficient bound propagation with per-neuron split constraints for neural network robustness verification. In: Proceedings of the 35th Conference on Neural Information Processing Systems (NeurIPS (2021)"},{"key":"6_CR70","doi-asserted-by":"crossref","unstructured":"Wu, H., et al.: Marabou 2.0: a versatile formal analyzer of neural networks. In: Proceedings of the 36th International Conference on Computer Aided Verification (CAV) (2024)","DOI":"10.1007\/978-3-031-65630-9_13"},{"key":"6_CR71","doi-asserted-by":"crossref","unstructured":"Yang, Y., Hu, H., Wei, T., Li, S.E., Liu, C.: Scalable synthesis of formally verified neural value function for Hamilton-Jacobi reachability analysis. J. Artif. Intell. Res. 83 (2025)","DOI":"10.1613\/jair.1.16946"},{"key":"6_CR72","unstructured":"Zhang, H., Shinn, M., Gupta, A., Gurfinkel, A., Le, N., Narodytska, N.: Verification of recurrent neural networks for cognitive tasks via reachability analysis. In: Proceedings of the 24th European Conference on Artificial Intelligence (ECAI), pp. 1690\u20131697 (2020)"},{"key":"6_CR73","unstructured":"Zhou, D., Brix, C., Hanasusanto, G.A., Zhang, H.: Scalable neural network verification with branch-and-bound inferred cutting planes. In: Proceedings of the 38th Conferenc on Neural Information Processing Systems (NeurIPS) (2024)"},{"key":"6_CR74","unstructured":"Zombori, D., B\u00e1nhelyi, B., Csendes, T., Megyeri, I., Jelasity, M.: Fooling a complete neural network verifier. In: Proceedings of the 9th International Conference on Learning Representations (ICLR) (2021)"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-15700-3_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,1,13]],"date-time":"2026-01-13T12:30:34Z","timestamp":1768307434000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-15700-3_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032156990","9783032157003"],"references-count":74,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-15700-3_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"13 January 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"VMCAI","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Verification, Model Checking, and Abstract Interpretation","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Rennes","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12 January 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 January 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"vmcai2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/home\/VMCAI-2026","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}