{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,28]],"date-time":"2026-03-28T20:31:40Z","timestamp":1774729900578,"version":"3.50.1"},"reference-count":70,"publisher":"Springer Science and Business Media LLC","issue":"19","license":[{"start":{"date-parts":[[2024,7,31]],"date-time":"2024-07-31T00:00:00Z","timestamp":1722384000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,7,31]],"date-time":"2024-07-31T00:00:00Z","timestamp":1722384000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/100014810","name":"Fondazione di Sardegna","doi-asserted-by":"publisher","award":["CUP J85F21001000005"],"award-info":[{"award-number":["CUP J85F21001000005"]}],"id":[{"id":"10.13039\/100014810","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100005642","name":"Universit\u00e0 degli Studi di Sassari","doi-asserted-by":"publisher","award":["FAR2020PULINAL"],"award-info":[{"award-number":["FAR2020PULINAL"]}],"id":[{"id":"10.13039\/501100005642","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Soft Comput"],"published-print":{"date-parts":[[2024,10]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    <jats:sc>NeVer2<\/jats:sc>\n                    is an open-source, cross-platform tool aimed at designing, training, and verifying neural networks. It seamlessly integrates popular learning libraries with our verification backend, offering their functionalities via a graphical interface. Users can design the structure of a neural network by intuitively arranging blocks on a canvas. Subsequently, network training involves specifying dataset sources and hyperparameters through dialog boxes. After training, the verification process entails two steps: (i) incorporating input preconditions and output postconditions via dedicated blocks, and (ii) initiating verification with a simple \u201cpush-button\u201d action. To our knowledge, there is currently no other publicly available tool that encompasses all these features. In this paper, we present a comprehensive description of\n                    <jats:sc>NeVer2<\/jats:sc>\n                    , illustrating its complete integration of design, training, and verification through examples. Additionally, we conduct experimental analyses on various verification benchmarks to illustrate the trade-off between completeness and computability using different algorithms. We also include a comparison with state-of-the-art tools such as\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$$\\alpha $$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:mi>\u03b1<\/mml:mi>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    ,\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$$\\beta $$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:mi>\u03b2<\/mml:mi>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    <jats:sc>-CROWN<\/jats:sc>\n                    and\n                    <jats:sc>NNV<\/jats:sc>\n                    for reference.\n                  <\/jats:p>","DOI":"10.1007\/s00500-024-09907-5","type":"journal-article","created":{"date-parts":[[2024,7,31]],"date-time":"2024-07-31T14:40:56Z","timestamp":1722436856000},"page":"11647-11665","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["NeVer2: learning and verification of neural networks"],"prefix":"10.1007","volume":"28","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4532-4933","authenticated-orcid":false,"given":"Stefano","family":"Demarchi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8284-5266","authenticated-orcid":false,"given":"Dario","family":"Guidotti","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0258-3222","authenticated-orcid":false,"given":"Luca","family":"Pulina","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9487-331X","authenticated-orcid":false,"given":"Armando","family":"Tacchella","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,7,31]]},"reference":[{"key":"9907_CR1","unstructured":"Abadi M, Barham P, Chen J, et\u00a0al (2016) Tensorflow: a system for large-scale machine learning. In: 12th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2016, Savannah, GA, USA, November 2-4, 2016. USENIX Association, pp 265\u2013283"},{"issue":"5","key":"9907_CR2","doi-asserted-by":"publisher","first-page":"2657","DOI":"10.1007\/s00500-020-05424-3","volume":"27","author":"AS Al-Waisy","year":"2023","unstructured":"Al-Waisy AS, Al-Fahdawi S, Mohammed MA et al (2023) Covid-chexnet: hybrid deep learning framework for identifying COVID-19 virus in chest x-rays images. Soft Comput 27(5):2657\u20132672. https:\/\/doi.org\/10.1007\/s00500-020-05424-3","journal-title":"Soft Comput"},{"key":"9907_CR3","doi-asserted-by":"publisher","unstructured":"Bak S (2021) nnenum: Verification of relu neural networks with optimized abstraction refinement. In: NASA Formal Methods - 13th International Symposium, NFM 2021, Virtual Event, May 24-28, 2021. Proceedings, Lecture Notes in Computer Science, vol 12673. Springer, pp 19\u201336. https:\/\/doi.org\/10.1007\/978-3-030-76384-8_2","DOI":"10.1007\/978-3-030-76384-8_2"},{"key":"9907_CR4","doi-asserted-by":"publisher","unstructured":"Bak S, Duggirala PS (2017) Simulation-equivalent reachability of large linear systems with inputs. In: Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017. Proceedings, Part I, Lecture Notes in Computer Science, vol 10426. Springer, pp 401\u2013420. https:\/\/doi.org\/10.1007\/978-3-319-63387-9_20","DOI":"10.1007\/978-3-319-63387-9_20"},{"key":"9907_CR5","doi-asserted-by":"publisher","unstructured":"Bak S, Tran H, Hobbs K, et\u00a0al (2020) Improved geometric path enumeration for verifying relu neural networks. In: Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part I, Lecture Notes in Computer Science, vol 12224. Springer, pp 66\u201396. https:\/\/doi.org\/10.1007\/978-3-030-53288-8_4","DOI":"10.1007\/978-3-030-53288-8_4"},{"key":"9907_CR6","unstructured":"Barrett C, Stump A, Tinelli C (2010) The SMT-LIB Standard: Version 2.0. In: Proceedings of the 8th International Workshop on Satisfiability Modulo Theories (Edinburgh, UK), p\u00a014"},{"key":"9907_CR7","doi-asserted-by":"publisher","unstructured":"Botoeva E, Kouvaros P, Kronqvist J, et\u00a0al (2020) Efficient verification of relu-based neural networks via dependency analysis. In: The Thirty-Fourth AAAI Conference on Artificial Intelligence, AAAI 2020, The Thirty-Second Innovative Applications of Artificial Intelligence Conference, IAAI 2020, The Tenth AAAI Symposium on Educational Advances in Artificial Intelligence, EAAI 2020, New York, NY, USA, February 7-12, 2020. AAAI Press, pp 3291\u20133299. https:\/\/doi.org\/10.1609\/AAAI.V34I04.5729","DOI":"10.1609\/AAAI.V34I04.5729"},{"key":"9907_CR8","unstructured":"Brix C, Noll T (2020) Debona: decoupled boundary network analysis for tighter bounds and faster adversarial robustness proofs. CoRR abs\/2006.09040"},{"key":"9907_CR9","unstructured":"Chappat E (2023) AiFiddle.io. https:\/\/aifiddle.io"},{"issue":"7","key":"9907_CR10","doi-asserted-by":"publisher","first-page":"2089","DOI":"10.1007\/s13042-022-01566-y","volume":"13","author":"Y Chen","year":"2022","unstructured":"Chen Y, Guo J, Huang J et al (2022) A novel method for financial distress prediction based on sparse neural networks with l$${}_{{1\/2}}$$ regularization. Int J Mach Learn Cybern 13(7):2089\u20132103. https:\/\/doi.org\/10.1007\/s13042-022-01566-y","journal-title":"Int J Mach Learn Cybern"},{"key":"9907_CR11","unstructured":"Cohen J, Rosenfeld E, Kolter JZ (2019) Certified adversarial robustness via randomized smoothing. In: 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. PMLR, pp 1310\u20131320"},{"issue":"5","key":"9907_CR12","doi-asserted-by":"publisher","first-page":"2635","DOI":"10.1007\/s00500-020-05275-y","volume":"27","author":"D Dansana","year":"2023","unstructured":"Dansana D, Kumar R, Bhattacharjee A et al (2023) Early diagnosis of covid-19-affected patients based on x-ray and computed tomography images using deep learning algorithm. Soft Comput 27(5):2635\u20132643. https:\/\/doi.org\/10.1007\/s00500-020-05275-y","journal-title":"Soft Comput"},{"key":"9907_CR13","doi-asserted-by":"publisher","DOI":"10.1007\/s00500-023-07918-2","author":"S Dash","year":"2023","unstructured":"Dash S, Parida P, Mohanty JR (2023) Illumination robust deep convolutional neural network for medical image classification. Soft Comput. https:\/\/doi.org\/10.1007\/s00500-023-07918-2","journal-title":"Soft Comput"},{"key":"9907_CR14","unstructured":"Demarchi S (2023) Experimenting with constraint programming techniques in artificial intelligence: automated system design and verification of neural networks. PhD thesis, University of Genoa, Italy. https:\/\/hdl.handle.net\/11567\/1117675"},{"key":"9907_CR15","doi-asserted-by":"publisher","unstructured":"Demarchi S, Guidotti D, Pitto A, et\u00a0al (2022) Formal verification of neural networks: A case study about adaptive cruise control. In: Hameed IA, Hasan A, Alaliyat SA (eds) Proceedings of the 36th ECMS International Conference on Modelling and Simulation, ECMS 2022, \u00c5lesund, Norway, May 30 - June 3, 2022. European Council for Modeling and Simulation, pp 310\u2013316. https:\/\/doi.org\/10.7148\/2022-0310","DOI":"10.7148\/2022-0310"},{"key":"9907_CR16","doi-asserted-by":"publisher","unstructured":"Demarchi S, Guidotti D, Pulina L, et\u00a0al (2023) Supporting standardization of neural networks verification with vnnlib and coconet. In: Proceedings of the 6th Workshop on Formal Methods for ML-Enabled Autonomous Systems, Kalpa Publications in Computing, vol\u00a016. EasyChair, pp 47\u201358. https:\/\/doi.org\/10.29007\/5pdh","DOI":"10.29007\/5pdh"},{"key":"9907_CR17","doi-asserted-by":"publisher","unstructured":"Eaton-Rosen Z, Bragman FJS, Bisdas S, et\u00a0al (2018) Towards safe deep learning: Accurately quantifying biomarker uncertainty in neural network predictions. In: Medical Image Computing and Computer Assisted Intervention - MICCAI 2018 - 21st International Conference, Granada, Spain, September 16-20, 2018, Proceedings, Part I, Lecture Notes in Computer Science, vol 11070. Springer, pp 691\u2013699. https:\/\/doi.org\/10.1007\/978-3-030-00928-1_78","DOI":"10.1007\/978-3-030-00928-1_78"},{"key":"9907_CR18","unstructured":"Eramo R, Fanni T, Guidotti D, et\u00a0al (2022) Verification of neural networks: challenges and perspectives in the aidoart project (short paper). In: Proceedings of the 10th Italian workshop on Planning and Scheduling (IPS 2022), RCRA Incontri E Confronti (RiCeRcA 2022), and the workshop on Strategies, Prediction, Interaction, and Reasoning in Italy (SPIRIT 2022) co-located with 21st International Conference of the Italian Association for Artificial Intelligence (AIxIA 2022), November 28 - December 2, 2022, University of Udine, Udine, Italy, CEUR Workshop Proceedings, vol 3345. CEUR-WS.org"},{"key":"9907_CR19","unstructured":"Ferrari C, M\u00fcller MN, Jovanovic N, et\u00a0al (2022) Complete verification via multi-neuron relaxation guided branch-and-bound. In: The Tenth International Conference on Learning Representations, ICLR 2022, Virtual Event, April 25-29, 2022. OpenReview.net"},{"key":"9907_CR20","doi-asserted-by":"publisher","unstructured":"Gehr T, Mirman M, Drachsler-Cohen D, et\u00a0al (2018) AI2: safety and robustness certification of neural networks with abstract interpretation. In: 2018 IEEE Symposium on Security and Privacy, SP 2018, Proceedings, 21-23 May 2018, San Francisco, California, USA. IEEE Computer Society, pp 3\u201318. https:\/\/doi.org\/10.1109\/SP.2018.00058","DOI":"10.1109\/SP.2018.00058"},{"key":"9907_CR21","unstructured":"Girard-Satabin J, Alberti M, Bobot F, et\u00a0al (2022) CAISAR: a platform for characterizing artificial intelligence safety and robustness. In: Proceedings of the Workshop on Artificial Intelligence Safety 2022 (AISafety 2022) co-located with the Thirty-First International Joint Conference on Artificial Intelligence and the Twenty-Fifth European Conference on Artificial Intelligence (IJCAI-ECAI-2022), Vienna, Austria, July 24-25, 2022, CEUR Workshop Proceedings, vol 3215. CEUR-WS.org"},{"key":"9907_CR22","doi-asserted-by":"publisher","first-page":"759","DOI":"10.1613\/JAIR.1.12850","volume":"72","author":"E Giunchiglia","year":"2021","unstructured":"Giunchiglia E, Lukasiewicz T (2021) Multi-label classification neural networks with hard logical constraints. J Artif Intell Res 72:759\u2013818. https:\/\/doi.org\/10.1613\/JAIR.1.12850","journal-title":"J Artif Intell Res"},{"key":"9907_CR23","doi-asserted-by":"publisher","unstructured":"Giunchiglia E, Stoian MC, Lukasiewicz T (2022) Deep learning with logical constraints. In: Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence, IJCAI 2022, Vienna, Austria, 23-29 July 2022. ijcai.org, pp 5478\u20135485. https:\/\/doi.org\/10.24963\/IJCAI.2022\/767","DOI":"10.24963\/IJCAI.2022\/767"},{"key":"9907_CR24","unstructured":"Goodfellow IJ, Shlens J, Szegedy C (2015) Explaining and harnessing adversarial examples. In: 3rd International Conference on Learning Representations, ICLR 2015, San Diego, CA, USA, May 7-9, 2015, Conference Track Proceedings"},{"key":"9907_CR25","doi-asserted-by":"publisher","unstructured":"Guidotti D, Leofante F, Castellini C, et\u00a0al (2019a) Repairing learned controllers with convex optimization: a case study. In: Integration of Constraint Programming, Artificial Intelligence, and Operations Research - 16th International Conference, CPAIOR 2019, Thessaloniki, Greece, June 4-7, 2019, Proceedings, Lecture Notes in Computer Science, vol 11494. Springer, pp 364\u2013373. https:\/\/doi.org\/10.1007\/978-3-030-19212-9_24","DOI":"10.1007\/978-3-030-19212-9_24"},{"key":"9907_CR26","doi-asserted-by":"publisher","unstructured":"Guidotti D, Leofante F, Pulina L, et\u00a0al (2019b) Verification and repair of neural networks: a progress report on convolutional models. In: AI*IA 2019 - Advances in Artificial Intelligence - XVIIIth International Conference of the Italian Association for Artificial Intelligence, Rende, Italy, November 19-22, 2019, Proceedings, Lecture Notes in Computer Science, vol 11946. Springer, pp 405\u2013417. https:\/\/doi.org\/10.1007\/978-3-030-35166-3_29","DOI":"10.1007\/978-3-030-35166-3_29"},{"key":"9907_CR27","doi-asserted-by":"publisher","unstructured":"Guidotti D, Leofante F, Pulina L, et\u00a0al (2020) Verification of neural networks: Enhancing scalability through pruning. In: ECAI 2020\u201424th European Conference on Artificial Intelligence, 29 August-8 September 2020, Santiago de Compostela, Spain, August 29 - September 8, 2020 - Including 10th Conference on Prestigious Applications of Artificial Intelligence (PAIS 2020), Frontiers in Artificial Intelligence and Applications, vol 325. IOS Press, pp 2505\u20132512. https:\/\/doi.org\/10.3233\/FAIA200384","DOI":"10.3233\/FAIA200384"},{"key":"9907_CR28","doi-asserted-by":"publisher","unstructured":"Guidotti D, Pulina L, Tacchella A (2021) pynever: a framework for learning and verification of neural networks. In: Automated Technology for Verification and Analysis - 19th International Symposium, ATVA 2021, Gold Coast, QLD, Australia, October 18-22, 2021, Proceedings, Lecture Notes in Computer Science, vol 12971. Springer, pp 357\u2013363. https:\/\/doi.org\/10.1007\/978-3-030-88885-5_23","DOI":"10.1007\/978-3-030-88885-5_23"},{"key":"9907_CR29","unstructured":"Guidotti D (2022) Verification of neural networks for safety and security-critical domains. In: Proceedings of the 10th Italian workshop on Planning and Scheduling (IPS 2022), RCRA Incontri E Confronti (RiCeRcA 2022), and the workshop on Strategies, Prediction, Interaction, and Reasoning in Italy (SPIRIT 2022) co-located with 21st International Conference of the Italian Association for Artificial Intelligence (AIxIA 2022), November 28 - December 2, 2022, University of Udine, Udine, Italy, CEUR Workshop Proceedings, vol 3345. CEUR-WS.org"},{"key":"9907_CR30","doi-asserted-by":"publisher","unstructured":"Guidotti D, Masiero R, Pandolfo L, et\u00a0al (2023a) Vector reconstruction error for anomaly detection: preliminary results in the IMOCO4.E project. In: 28th IEEE International Conference on Emerging Technologies and Factory Automation, ETFA 2023, Sinaia, Romania, September 12-15, 2023. IEEE, pp 1\u20134. https:\/\/doi.org\/10.1109\/ETFA54631.2023.10275396","DOI":"10.1109\/ETFA54631.2023.10275396"},{"key":"9907_CR31","doi-asserted-by":"publisher","unstructured":"Guidotti D, Pandolfo L, Pulina L (2023b) Detection of component degradation: A study on autoencoder-based approaches. In: 19th IEEE International Conference on e-Science, e-Science 2023, Limassol, Cyprus, October 9-13, 2023. IEEE, pp 1\u20132. https:\/\/doi.org\/10.1109\/E-SCIENCE58273.2023.10254890","DOI":"10.1109\/E-SCIENCE58273.2023.10254890"},{"issue":"7","key":"9907_CR32","doi-asserted-by":"publisher","first-page":"397","DOI":"10.3390\/INFO14070397","volume":"14","author":"D Guidotti","year":"2023","unstructured":"Guidotti D, Pandolfo L, Pulina L (2023) Leveraging satisfiability modulo theory solvers for verification of neural networks in predictive maintenance applications. Information 14(7):397. https:\/\/doi.org\/10.3390\/INFO14070397","journal-title":"Information"},{"key":"9907_CR33","doi-asserted-by":"publisher","unstructured":"Guidotti D, Pandolfo L, Pulina L (2023d) Verification of nns in the IMOCO4.E project: Preliminary results. In: 28th IEEE International Conference on Emerging Technologies and Factory Automation, ETFA 2023, Sinaia, Romania, September 12-15, 2023. IEEE, pp 1\u20134. https:\/\/doi.org\/10.1109\/ETFA54631.2023.10275345","DOI":"10.1109\/ETFA54631.2023.10275345"},{"key":"9907_CR34","doi-asserted-by":"publisher","unstructured":"Guidotti D, Pandolfo L, Pulina L (2023e) Verifying neural networks with SMT: an experimental evaluation. In: 19th IEEE International Conference on e-Science, e-Science 2023, Limassol, Cyprus, October 9-13, 2023. IEEE, pp 1\u20132. https:\/\/doi.org\/10.1109\/E-SCIENCE58273.2023.10254877","DOI":"10.1109\/E-SCIENCE58273.2023.10254877"},{"issue":"11","key":"9907_CR35","doi-asserted-by":"publisher","first-page":"7179","DOI":"10.1007\/s00500-023-07945-z","volume":"27","author":"Y Gul","year":"2023","unstructured":"Gul Y, M\u00fcezzinoglu T, Kilicarslan G et al (2023) Application of the deep transfer learning framework for hydatid cyst classification using CT images. Soft Comput 27(11):7179\u20137189. https:\/\/doi.org\/10.1007\/s00500-023-07945-z","journal-title":"Soft Comput"},{"key":"9907_CR36","doi-asserted-by":"publisher","unstructured":"Henriksen P, Lomuscio AR (2020) Efficient neural network verification via adaptive refinement and adversarial search. In: ECAI 2020 - 24th European Conference on Artificial Intelligence, 29 August-8 September 2020, Santiago de Compostela, Spain, August 29 - September 8, 2020 - Including 10th Conference on Prestigious Applications of Artificial Intelligence (PAIS 2020), Frontiers in Artificial Intelligence and Applications, vol 325. IOS Press, pp 2513\u20132520. https:\/\/doi.org\/10.3233\/FAIA200385","DOI":"10.3233\/FAIA200385"},{"key":"9907_CR37","doi-asserted-by":"publisher","unstructured":"Henriksen P, Lomuscio A (2021) DEEPSPLIT: an efficient splitting method for neural network verification via indirect effect analysis. In: Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence, IJCAI 2021, Virtual Event \/ Montreal, Canada, 19-27 August 2021. ijcai.org, pp 2549\u20132555. https:\/\/doi.org\/10.24963\/IJCAI.2021\/351","DOI":"10.24963\/IJCAI.2021\/351"},{"key":"9907_CR38","doi-asserted-by":"publisher","unstructured":"Henriksen P, Leofante F, Lomuscio A (2022) Repairing misclassifications in neural networks using limited data. In: SAC \u201922: The 37th ACM\/SIGAPP Symposium on Applied Computing, Virtual Event, April 25 - 29, 2022. ACM, pp 1031\u20131038. https:\/\/doi.org\/10.1145\/3477314.3507059","DOI":"10.1145\/3477314.3507059"},{"issue":"5","key":"9907_CR39","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1016\/0893-6080(89)90020-8","volume":"2","author":"K Hornik","year":"1989","unstructured":"Hornik K, Stinchcombe MB, White H (1989) Multilayer feedforward networks are universal approximators. Neural Netw 2(5):359\u2013366. https:\/\/doi.org\/10.1016\/0893-6080(89)90020-8","journal-title":"Neural Netw"},{"key":"9907_CR40","doi-asserted-by":"publisher","unstructured":"Hu Z, Ma X, Liu Z, et\u00a0al (2016) Harnessing deep neural networks with logic rules. In: Proceedings of the 54th Annual Meeting of the Association for Computational Linguistics, ACL 2016, August 7-12, 2016, Berlin, Germany, Volume 1: Long Papers. The Association for Computer Linguistics. https:\/\/doi.org\/10.18653\/V1\/P16-1228","DOI":"10.18653\/V1\/P16-1228"},{"issue":"19","key":"9907_CR41","doi-asserted-by":"publisher","first-page":"14063","DOI":"10.1007\/s00500-023-07922-6","volume":"27","author":"H Jahanbakhti","year":"2023","unstructured":"Jahanbakhti H, Pourgholi M, Yazdizadeh A (2023) Online neural network-based model reduction and switching fuzzy control of a nonlinear large-scale fractional-order system. Soft Comput 27(19):14063\u201314071. https:\/\/doi.org\/10.1007\/s00500-023-07922-6","journal-title":"Soft Comput"},{"key":"9907_CR42","doi-asserted-by":"crossref","unstructured":"Joseph FJJ, Nonsiri S, Monsakul A (2021) Keras and tensorflow: A hands-on experience. In: A Practical Approach, Advanced Deep Learning for Engineers and Scientists, pp. 85\u2013111","DOI":"10.1007\/978-3-030-66519-7_4"},{"key":"9907_CR43","doi-asserted-by":"publisher","unstructured":"Katz G, Barrett CW, Dill DL, et\u00a0al (2017) Reluplex: an efficient SMT solver for verifying deep neural networks. In: Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I, Lecture Notes in Computer Science, vol 10426. Springer, pp 97\u2013117. https:\/\/doi.org\/10.1007\/978-3-319-63387-9_5","DOI":"10.1007\/978-3-319-63387-9_5"},{"key":"9907_CR44","doi-asserted-by":"publisher","unstructured":"Katz G, Huang DA, Ibeling D, et\u00a0al (2019) The marabou framework for verification and analysis of deep neural networks. In: Computer Aided Verification\u201431st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part I, Lecture Notes in Computer Science, vol 11561. Springer, pp 443\u2013452, https:\/\/doi.org\/10.1007\/978-3-030-25540-4_26","DOI":"10.1007\/978-3-030-25540-4_26"},{"key":"9907_CR45","unstructured":"Kingma DP, Ba J (2015) Adam: a method for stochastic optimization. In: 3rd International Conference on Learning Representations, ICLR 2015, San Diego, CA, USA, May 7-9, 2015, Conference Track Proceedings"},{"key":"9907_CR46","doi-asserted-by":"publisher","unstructured":"Kouvaros P, Kyono T, Leofante F, et\u00a0al (2021) Formal analysis of neural network-based systems in the aircraft domain. In: Formal Methods - 24th International Symposium, FM 2021, Virtual Event, November 20-26, 2021, Proceedings, Lecture Notes in Computer Science, vol 13047. Springer, pp 730\u2013740. https:\/\/doi.org\/10.1007\/978-3-030-90870-6_41","DOI":"10.1007\/978-3-030-90870-6_41"},{"key":"9907_CR47","doi-asserted-by":"publisher","unstructured":"LeNail A (2019) NN-SVG: publication-ready neural network architecture schematics. J Open Source Softw 4(33):747. https:\/\/doi.org\/10.21105\/JOSS.00747","DOI":"10.21105\/JOSS.00747"},{"key":"9907_CR48","doi-asserted-by":"publisher","unstructured":"Leofante F, Henriksen P, Lomuscio A (2023) Verification-friendly networks: the case for parametric relus. In: International Joint Conference on Neural Networks, IJCNN 2023, Gold Coast, Australia, June 18-23, 2023. IEEE, pp 1\u20139, https:\/\/doi.org\/10.1109\/IJCNN54540.2023.10191169","DOI":"10.1109\/IJCNN54540.2023.10191169"},{"key":"9907_CR49","doi-asserted-by":"publisher","unstructured":"M\u00fcller MN, Brix C, Bak S, et\u00a0al (2022) The third international verification of neural networks competition (VNN-COMP 2022): summary and results. CoRR abs\/2212.10376. https:\/\/doi.org\/10.48550\/ARXIV.2212.10376","DOI":"10.48550\/ARXIV.2212.10376"},{"key":"9907_CR50","unstructured":"Nagisetty V (2021) Domain knowledge guided testing and training of neural networks. Master\u2019s thesis, University of Waterloo"},{"key":"9907_CR51","unstructured":"Paszke A, Gross S, Massa F, et\u00a0al (2019) Pytorch: an imperative style, high-performance deep learning library. In: Advances in Neural Information Processing Systems 32: Annual Conference on Neural Information Processing Systems 2019, NeurIPS 2019, December 8-14, 2019, Vancouver, BC, Canada, pp 8024\u20138035"},{"key":"9907_CR52","doi-asserted-by":"publisher","DOI":"10.1007\/s00500-023-07936-0","author":"A Pavithra","year":"2023","unstructured":"Pavithra A, Kalpana G, Vigneswaran T (2023) Deep learning-based automated disease detection and classification model for precision agriculture. Soft Comput. https:\/\/doi.org\/10.1007\/s00500-023-07936-0","journal-title":"Soft Comput"},{"key":"9907_CR53","doi-asserted-by":"publisher","unstructured":"Pulina L, Tacchella A (2010) An abstraction-refinement approach to verification of artificial neural networks. In: Computer Aided Verification, 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010. Proceedings, Lecture Notes in Computer Science, vol 6174. Springer, pp 243\u2013257, https:\/\/doi.org\/10.1007\/978-3-642-14295-6_24","DOI":"10.1007\/978-3-642-14295-6_24"},{"key":"9907_CR54","unstructured":"Roeder L (2023) Netron.app. https:\/\/netron.app"},{"issue":"5","key":"9907_CR55","doi-asserted-by":"publisher","first-page":"657","DOI":"10.3390\/e24050657","volume":"24","author":"K Sako","year":"2022","unstructured":"Sako K, Mpinda BN, Rodrigues PC (2022) Neural networks for financial time series forecasting. Entropy 24(5):657. https:\/\/doi.org\/10.3390\/e24050657","journal-title":"Entropy"},{"key":"9907_CR56","doi-asserted-by":"publisher","unstructured":"Seide F, Agarwal A (2016) CNTK: microsoft\u2019s open-source deep-learning toolkit. In: Proceedings of the 22nd ACM SIGKDD International Conference on Knowledge Discovery and Data Mining, San Francisco, CA, USA, August 13-17, 2016. ACM, p 2135, https:\/\/doi.org\/10.1145\/2939672.2945397","DOI":"10.1145\/2939672.2945397"},{"key":"9907_CR57","doi-asserted-by":"publisher","unstructured":"Singh G, Gehr T, P\u00fcschel M, et\u00a0al (2019a) An abstract domain for certifying neural networks. Proc ACM Program Lang 3(POPL):41:1\u201341:30. https:\/\/doi.org\/10.1145\/3290354","DOI":"10.1145\/3290354"},{"key":"9907_CR58","unstructured":"Singh G, Gehr T, P\u00fcschel M, et\u00a0al (2019b) Boosting robustness certification of neural networks. In: 7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019. OpenReview.net"},{"key":"9907_CR59","doi-asserted-by":"publisher","unstructured":"Sotoudeh M, Thakur AV (2021) Provable repair of deep neural networks. In: PLDI \u201921: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Virtual Event, Canada, June 20-25, 2021. ACM, pp 588\u2013603, https:\/\/doi.org\/10.1145\/3453483.3454064","DOI":"10.1145\/3453483.3454064"},{"key":"9907_CR60","unstructured":"Szegedy C, Zaremba W, Sutskever I, et\u00a0al (2014) Intriguing properties of neural networks. In: 2nd International Conference on Learning Representations, ICLR 2014, Banff, AB, Canada, April 14-16, 2014, Conference Track Proceedings"},{"key":"9907_CR61","unstructured":"Tjeng V, Xiao KY, Tedrake R (2019) Evaluating robustness of neural networks with mixed integer programming. In: 7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019. OpenReview.net"},{"key":"9907_CR62","doi-asserted-by":"publisher","unstructured":"Tran H, Lopez DM, Musau P, et\u00a0al (2019) Star-based reachability analysis of deep neural networks. In: Formal Methods - The Next 30 Years - Third World Congress, FM 2019, Porto, Portugal, October 7-11, 2019, Proceedings, Lecture Notes in Computer Science, vol 11800. Springer, pp 670\u2013686, https:\/\/doi.org\/10.1007\/978-3-030-30942-8_39","DOI":"10.1007\/978-3-030-30942-8_39"},{"key":"9907_CR63","doi-asserted-by":"publisher","unstructured":"Tran H, Yang X, Lopez DM, et\u00a0al (2020) NNV: the neural network verification tool for deep neural networks and learning-enabled cyber-physical systems. In: Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part I, Lecture Notes in Computer Science, vol 12224. Springer, pp 3\u201317, https:\/\/doi.org\/10.1007\/978-3-030-53288-8_1","DOI":"10.1007\/978-3-030-53288-8_1"},{"key":"9907_CR64","unstructured":"Wang S, Zhang H, Xu K, et\u00a0al (2021) Beta-crown: efficient bound propagation with per-neuron split constraints for neural network robustness verification. In: Advances in Neural Information Processing Systems 34: Annual Conference on Neural Information Processing Systems 2021, NeurIPS 2021, December 6-14, 2021, virtual, pp 29,909\u201329,921"},{"key":"9907_CR65","unstructured":"Xu K, Zhang H, Wang S, et\u00a0al (2021) Fast and complete: enabling complete neural network verification with rapid and massively parallel incomplete verifiers. In: 9th International Conference on Learning Representations, ICLR 2021, Virtual Event, Austria, May 3-7, 2021. OpenReview.net"},{"issue":"6","key":"9907_CR66","doi-asserted-by":"publisher","first-page":"3461","DOI":"10.1007\/s00500-021-06113-5","volume":"27","author":"F Yang","year":"2023","unstructured":"Yang F, Chen J, Liu Y (2023) Improved and optimized recurrent neural network based on PSO and its application in stock price prediction. Soft Comput 27(6):3461\u20133476. https:\/\/doi.org\/10.1007\/s00500-021-06113-5","journal-title":"Soft Comput"},{"key":"9907_CR67","unstructured":"Zhang H, Weng T, Chen P, et\u00a0al (2018) Efficient neural network robustness certification with general activation functions. In: Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018, NeurIPS 2018, December 3-8, 2018, Montr\u00e9al, Canada, pp 4944\u20134953"},{"key":"9907_CR68","unstructured":"Zhang H, Wang S, Xu K, et\u00a0al (2022) General cutting planes for bound-propagation-based neural network verification. In: NeurIPS"},{"key":"9907_CR69","doi-asserted-by":"publisher","DOI":"10.1007\/s00500-023-07912-8","author":"B Zhang","year":"2023","unstructured":"Zhang B, Huang W, Zhao F (2023) An available-flow neural network for solving the dynamic groundwater network maximum flow problem. Soft Comput. https:\/\/doi.org\/10.1007\/s00500-023-07912-8","journal-title":"Soft Comput"},{"key":"9907_CR70","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1016\/J.CAD.2018.12.002","volume":"109","author":"Y Zheng","year":"2019","unstructured":"Zheng Y (2019) Computing bounding polytopes of a compact set and related problems in n-dimensional space. Comput Aided Des 109:22\u201332. https:\/\/doi.org\/10.1016\/J.CAD.2018.12.002","journal-title":"Comput Aided Des"}],"container-title":["Soft Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00500-024-09907-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00500-024-09907-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00500-024-09907-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,19]],"date-time":"2024-10-19T03:13:34Z","timestamp":1729307614000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s00500-024-09907-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,7,31]]},"references-count":70,"journal-issue":{"issue":"19","published-print":{"date-parts":[[2024,10]]}},"alternative-id":["9907"],"URL":"https:\/\/doi.org\/10.1007\/s00500-024-09907-5","relation":{"has-preprint":[{"id-type":"doi","id":"10.21203\/rs.3.rs-3925432\/v1","asserted-by":"object"}]},"ISSN":["1432-7643","1433-7479"],"issn-type":[{"value":"1432-7643","type":"print"},{"value":"1433-7479","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,7,31]]},"assertion":[{"value":"23 May 2024","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"31 July 2024","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors have not disclosed any competing interests.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}}]}}