{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,1]],"date-time":"2026-04-01T17:59:38Z","timestamp":1775066378768,"version":"3.50.1"},"publisher-location":"Cham","reference-count":40,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031986789","type":"print"},{"value":"9783031986796","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,7,22]],"date-time":"2025-07-22T00:00:00Z","timestamp":1753142400000},"content-version":"vor","delay-in-days":202,"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":"Abstract<\/jats:title>\n Deep Neural Networks (DNNs) are increasingly deployed in critical applications, where ensuring their safety and robustness is paramount. We present \n \n $$_\\text {CAV25}$$<\/jats:tex-math>\n \n \n \n \n CAV<\/mml:mi>\n 25<\/mml:mn>\n <\/mml:mrow>\n <\/mml:msub>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula>, a high-performance DNN verification tool that uses the DPLL(T) framework and supports a wide-range of network architectures and activation functions. Since its debut in VNN-COMP\u201923, in which it achieved the New Participant Award and ranked 4th overall, \n \n $$_\\text {CAV25}$$<\/jats:tex-math>\n \n \n \n \n CAV<\/mml:mi>\n 25<\/mml:mn>\n <\/mml:mrow>\n <\/mml:msub>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula> has advanced significantly, achieving second place in VNN-COMP\u201924. This paper presents and evaluates the latest development of \n \n $$_\\text {CAV25}$$<\/jats:tex-math>\n \n \n \n \n CAV<\/mml:mi>\n 25<\/mml:mn>\n <\/mml:mrow>\n <\/mml:msub>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula>, focusing on the versatility, ease of use, and competitive performance of the tool. \n \n $$_\\text {CAV25}$$<\/jats:tex-math>\n \n \n \n \n CAV<\/mml:mi>\n 25<\/mml:mn>\n <\/mml:mrow>\n <\/mml:msub>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula> is available at: https:\/\/github.com\/dynaroars\/neuralsat<\/jats:ext-link>.<\/jats:p>","DOI":"10.1007\/978-3-031-98679-6_19","type":"book-chapter","created":{"date-parts":[[2025,7,21]],"date-time":"2025-07-21T09:21:17Z","timestamp":1753089677000},"page":"409-423","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["NeuralSAT: A High-Performance Verification Tool for\u00a0Deep Neural Networks"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3341-9794","authenticated-orcid":false,"given":"Hai","family":"Duong","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4255-4592","authenticated-orcid":false,"given":"ThanhVu","family":"Nguyen","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1937-1544","authenticated-orcid":false,"given":"Matthew B.","family":"Dwyer","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,7,22]]},"reference":[{"key":"19_CR1","doi-asserted-by":"publisher","unstructured":"Althoff, M.: An introduction to Cora 2015. In: Proceedings of the Workshop on Applied Verification for Continuous and Hybrid Systems, pp. 120\u2013151 (2015). https:\/\/doi.org\/10.29007\/zbkv","DOI":"10.29007\/zbkv"},{"key":"19_CR2","unstructured":"Bai, J., Lu, F., Zhang, K.: ONNX Open neural network exchange. https:\/\/onnx.ai"},{"key":"19_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/978-3-030-76384-8_2","volume-title":"NASA Formal Methods","author":"S Bak","year":"2021","unstructured":"Bak, S.: nnenum: verification of ReLU neural networks with optimized abstraction refinement. In: Dutle, A., Moscato, M.M., Titolo, L., Mu\u00f1oz, C.A., Perez, I. (eds.) NFM 2021. LNCS, vol. 12673, pp. 19\u201336. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-76384-8_2"},{"key":"19_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"405","DOI":"10.1007\/978-3-319-24318-4_29","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2015","author":"A Biere","year":"2015","unstructured":"Biere, A., Fr\u00f6hlich, A.: Evaluating CDCL variable scoring schemes. In: Heule, M., Weaver, S. (eds.) SAT 2015. LNCS, vol. 9340, pp. 405\u2013422. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-24318-4_29"},{"key":"19_CR5","doi-asserted-by":"publisher","unstructured":"Brix, C., Bak, S., Johnson, T.T., Wu, H.: The Fifth International Verification of Neural Networks Competition (VNN-COMP 2024): Summary and Results. arXiv preprint arXiv:2412.19985 (2024). https:\/\/doi.org\/10.48550\/arXiv.2412.19985","DOI":"10.48550\/arXiv.2412.19985"},{"key":"19_CR6","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 (2023). https:\/\/doi.org\/10.48550\/arXiv.2312.16760","DOI":"10.48550\/arXiv.2312.16760"},{"key":"19_CR7","doi-asserted-by":"publisher","unstructured":"Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Commun. ACM 5(7), 394\u2013397 (1962). https:\/\/doi.org\/10.1145\/368273.368557","DOI":"10.1145\/368273.368557"},{"key":"19_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"19_CR9","doi-asserted-by":"publisher","unstructured":"De\u00a0Palma, A., et al.: Improved branch and bound for neural network verification via Lagrangian decomposition. arXiv preprint arXiv:2104.06718 (2021). https:\/\/doi.org\/10.48550\/arXiv.2104.06718","DOI":"10.48550\/arXiv.2104.06718"},{"issue":"19","key":"19_CR10","doi-asserted-by":"publisher","first-page":"11647","DOI":"10.1007\/s00500-024-09907-5","volume":"28","author":"S Demarchi","year":"2024","unstructured":"Demarchi, S., Guidotti, D., Pulina, L., Tacchella, A.: Never2: learning and verification of neural networks. Soft. Comput. 28(19), 11647\u201311665 (2024). https:\/\/doi.org\/10.1007\/s00500-024-09907-5","journal-title":"Soft. Comput."},{"key":"19_CR11","unstructured":"dreal: An SMT Solver for Nonlinear Theories of Reals (2024). https:\/\/dreal.github.io\/"},{"key":"19_CR12","doi-asserted-by":"publisher","unstructured":"Duong, H., Nguyen, T., Dwyer, M.: A DPLL(T) Framework for Verifying Deep Neural Networks. arXiv preprint arXiv:2307.10266 (2024). https:\/\/doi.org\/10.48550\/arXiv.2307.10266","DOI":"10.48550\/arXiv.2307.10266"},{"key":"19_CR13","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","DOI":"10.1145\/3643765"},{"key":"19_CR14","unstructured":"ETH-SRI: ETH Robustness Analyzer for Deep Neural Networks (2021). https:\/\/github.com\/eth-sri\/eran"},{"key":"19_CR15","doi-asserted-by":"publisher","unstructured":"Ferrari, C., Mueller, M.N., Jovanovi\u0107, N., Vechev, M.: Complete Verification via Multi-Neuron Relaxation Guided Branch-and-Bound. In: International Conference on Learning Representations (2022). https:\/\/doi.org\/10.48550\/arXiv.2205.00263","DOI":"10.48550\/arXiv.2205.00263"},{"key":"19_CR16","unstructured":"FICO: Xpress Optimization (2024). https:\/\/www.fico.com\/en\/products\/fico-xpress-optimization"},{"key":"19_CR17","unstructured":"Gurobi Optimization, LLC: Gurobi Optimizer Reference Manual (2022). https:\/\/www.gurobi.com"},{"key":"19_CR18","doi-asserted-by":"publisher","DOI":"10.1016\/j.cosrev.2020.100270","volume":"37","author":"X Huang","year":"2020","unstructured":"Huang, X., et al.: A survey of safety and trustworthiness of deep neural networks: verification, testing, adversarial attack and defence, and interpretability. Comput. Sci. Rev. 37, 100270 (2020). https:\/\/doi.org\/10.1016\/j.cosrev.2020.100270","journal-title":"Comput. Sci. Rev."},{"key":"19_CR19","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":"19_CR20","doi-asserted-by":"publisher","unstructured":"Kroening, D., Strichman, O.: Decision procedures. Springer, Heidelberg (2008). https:\/\/doi.org\/10.5555\/1391237","DOI":"10.5555\/1391237"},{"key":"19_CR21","doi-asserted-by":"publisher","unstructured":"Liu, C., Arnon, T., Lazarus, C., Strong, C., Barrett, C., Kochenderfer, M.J., et\u00a0al.: Algorithms for verifying deep neural networks. Found. Trends\u00ae Optim. 4(3-4), 244\u2013404 (2021). https:\/\/doi.org\/10.1561\/2400000035","DOI":"10.1561\/2400000035"},{"key":"19_CR22","unstructured":"Madry, A., Makelov, A., Schmidt, L., Tsipras, D., Vladu, A.: Towards deep learning models resistant to adversarial attacks. arXiv preprint arXiv:1706.06083 (2017). https:\/\/hdl.handle.net\/1721.1\/137496"},{"key":"19_CR23","doi-asserted-by":"publisher","first-page":"417","DOI":"10.1109\/TSE.1981.230844","volume":"4","author":"J Misra","year":"1981","unstructured":"Misra, J., Chandy, K.M.: Proofs of networks of processes. IEEE Trans. Softw. Eng. 4, 417\u2013426 (1981). https:\/\/doi.org\/10.1109\/TSE.1981.230844","journal-title":"IEEE Trans. Softw. Eng."},{"key":"19_CR24","unstructured":"PyRAT: A tool to analyze the robustness and safety of neural networks (2024). https:\/\/pyrat-analyzer.com\/"},{"issue":"3","key":"19_CR25","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1016\/j.eng.2019.12.012","volume":"6","author":"K Ren","year":"2020","unstructured":"Ren, K., Zheng, T., Qin, Z., Liu, X.: Adversarial attacks and defenses in deep learning. Engineering 6(3), 346\u2013360 (2020). https:\/\/doi.org\/10.1016\/j.eng.2019.12.012","journal-title":"Engineering"},{"key":"19_CR26","unstructured":"Sorensson, N., Een, N.: Minisat v1. 13-a sat solver with conflict-clause minimization. SAT 2005(53), 1\u20132 (2005). https:\/\/api.semanticscholar.org\/CorpusID:63165862"},{"key":"19_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1007\/3-540-16042-6_21","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"EW Stark","year":"1985","unstructured":"Stark, E.W.: A proof technique for rely\/guarantee properties. In: Maheshwari, S.N. (ed.) FSTTCS 1985. LNCS, vol. 206, pp. 369\u2013391. Springer, Heidelberg (1985). https:\/\/doi.org\/10.1007\/3-540-16042-6_21"},{"key":"19_CR28","unstructured":"Tacchella, A., Pulina, L., Guidotti, D., Demarchi, S.: The international benchmarks standard for the Verification of Neural Networks (2023). https:\/\/www.vnnlib.org\/"},{"key":"19_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"670","DOI":"10.1007\/978-3-030-30942-8_39","volume-title":"Formal Methods \u2013 The Next 30 Years","author":"H-D Tran","year":"2019","unstructured":"Tran, H.-D., et al.: Star-based reachability analysis of deep neural networks. In: ter Beek, M.H., McIver, A., Oliveira, J.N. (eds.) FM 2019. LNCS, vol. 11800, pp. 670\u2013686. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-30942-8_39"},{"key":"19_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-030-53288-8_1","volume-title":"Computer Aided Verification","author":"H-D Tran","year":"2020","unstructured":"Tran, H.-D., et al.: NNV: the neural network verification tool for deep neural networks and learning-enabled cyber-physical systems. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12224, pp. 3\u201317. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53288-8_1"},{"key":"19_CR31","doi-asserted-by":"publisher","unstructured":"Urban, C., Min\u00e9, A.: A review of formal methods applied to machine learning. arXiv preprint arXiv:2104.02466 (2021). https:\/\/doi.org\/10.48550\/arXiv.2104.02466","DOI":"10.48550\/arXiv.2104.02466"},{"key":"19_CR32","doi-asserted-by":"publisher","unstructured":"Wang, S., et al.: Beta-CROWN: efficient bound propagation with per-neuron split constraints for complete and incomplete neural network robustness verification. Adv. Neural Inf. Process. Syst. 34, 29909\u201329921 (2021). https:\/\/doi.org\/10.48550\/arXiv.2103.06624","DOI":"10.48550\/arXiv.2103.06624"},{"key":"19_CR33","doi-asserted-by":"publisher","unstructured":"Wu, H., Isac, O., et\u00a0al.: Marabou 2.0: a versatile formal analyzer of neural networks. In: Gurfinkel, A., Ganesh, V. (eds.) International Conference on Computer Aided Verification, pp. 249\u2013264. Springer, Cham (2024). https:\/\/doi.org\/10.48550\/arXiv.2401.14461","DOI":"10.48550\/arXiv.2401.14461"},{"key":"19_CR34","doi-asserted-by":"publisher","unstructured":"Xu, D., Mozumder, N.J., Duong, H., Dwyer, M.: Training for verification: increasing neuron stability to scale DNN verification. In: Finkbeiner, B., Kov\u00e1cs, L. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2024. LNCS, vol. 14572, pp. 24\u201344. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-57256-2_2","DOI":"10.1007\/978-3-031-57256-2_2"},{"key":"19_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/978-3-030-53288-8_5","volume-title":"Computer Aided Verification","author":"D Xu","year":"2020","unstructured":"Xu, D., Shriver, D., Dwyer, M.B., Elbaum, S.: Systematic generation of diverse benchmarks for DNN verification. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12224, pp. 97\u2013121. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53288-8_5"},{"key":"19_CR36","doi-asserted-by":"publisher","unstructured":"Xu, K., et al.: Automatic perturbation analysis for scalable certified robustness and beyond. Adv. Neural Inf. Process. Syst. 33, 1129\u20131141 (2020). https:\/\/doi.org\/10.5555\/3495724.3495820","DOI":"10.5555\/3495724.3495820"},{"key":"19_CR37","doi-asserted-by":"publisher","unstructured":"Yang, Z., Shi, J., He, J., Lo, D.: Natural attack for pre-trained models of code. In: Proceedings of the 44th International Conference on Software Engineering, pp. 1482\u20131493 (2022). https:\/\/doi.org\/10.1145\/3510003.3510146","DOI":"10.1145\/3510003.3510146"},{"key":"19_CR38","doi-asserted-by":"publisher","unstructured":"Yu, Y., Qian, H., Hu, Y.Q.: Derivative-free optimization via classification. In: Thirtieth AAAI Conference on Artificial Intelligence (2016). https:\/\/doi.org\/10.5555\/3016100.3016218","DOI":"10.5555\/3016100.3016218"},{"key":"19_CR39","doi-asserted-by":"publisher","unstructured":"Zhang, T., Gao, C., Ma, L., Lyu, M., Kim, M.: An empirical study of common challenges in developing deep learning applications. In: 2019 IEEE 30th International Symposium on Software Reliability Engineering (ISSRE), pp. 104\u2013115. IEEE (2019). https:\/\/doi.org\/10.1109\/ISSRE.2019.00020","DOI":"10.1109\/ISSRE.2019.00020"},{"key":"19_CR40","doi-asserted-by":"publisher","unstructured":"Z\u00fcgner, D., Akbarnejad, A., G\u00fcnnemann, S.: Adversarial attacks on neural networks for graph data. In: Proceedings of the 24th ACM SIGKDD International Conference on Knowledge Discovery & Data Mining, vol. 2019-August, pp. 2847\u20132856. ACM, New York, NY, USA, July 2018. https:\/\/doi.org\/10.1145\/3219819.3220078","DOI":"10.1145\/3219819.3220078"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-98679-6_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,21]],"date-time":"2025-07-21T09:21:23Z","timestamp":1753089683000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-98679-6_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031986789","9783031986796"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-98679-6_19","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":"22 July 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Zagreb","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Croatia","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":"21 July 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 July 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"37","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conferences.i-cav.org\/2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}