{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T18:40:20Z","timestamp":1767984020731,"version":"3.49.0"},"publisher-location":"Cham","reference-count":43,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032107930","type":"print"},{"value":"9783032107947","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,11,16]],"date-time":"2025-11-16T00:00:00Z","timestamp":1763251200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,11,16]],"date-time":"2025-11-16T00:00:00Z","timestamp":1763251200000},"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-10794-7_15","type":"book-chapter","created":{"date-parts":[[2025,11,15]],"date-time":"2025-11-15T06:43:07Z","timestamp":1763188987000},"page":"290-309","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["The CAISAR Platform: Extending the Reach of Machine Learning Specification and Verification"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0001-4352-4555","authenticated-orcid":false,"given":"Michele","family":"Alberti","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6756-0788","authenticated-orcid":false,"given":"Fran\u00e7ois","family":"Bobot","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6374-3694","authenticated-orcid":false,"given":"Julien","family":"Girard-Satabin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8466-8777","authenticated-orcid":false,"given":"Alban","family":"Grastien","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0007-0829-9309","authenticated-orcid":false,"given":"Aymeric","family":"Varasse","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0004-8915-4774","authenticated-orcid":false,"given":"Zakaria","family":"Chihani","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,11,16]]},"reference":[{"key":"15_CR1","unstructured":"Alberti, M., Bobot, F., Chihani, Z., Girard-Satabin, J., Lemesle, A.: CAISAR: a platform for characterizing artificial intelligence safety and robustness. In: AISafety. CEUR-Workshop Proceedings, Vienne, Austria (2022). https:\/\/hal.archives-ouvertes.fr\/hal-03687211"},{"key":"15_CR2","doi-asserted-by":"publisher","unstructured":"Athavale, A., Bartocci, E., Christakis, M., Maffei, M., Nickovic, D., Weissenbacher, G.: Verifying global two-safety properties in neural networks with confidence. In: Gurfinkel, A., Ganesh, V. (eds.) Computer Aided Verification, pp. 329\u2013351. Springer Nature Switzerland, Cham (Jun 2024). https:\/\/doi.org\/10.48550\/arXiv.2405.14400, http:\/\/arxiv.org\/abs\/2405.14400, zSCC: 0000000 arXiv:2405.14400 [cs] type: article","DOI":"10.48550\/arXiv.2405.14400"},{"key":"15_CR3","doi-asserted-by":"publisher","DOI":"10.3233\/faia240600","author":"G Audemard","year":"2024","unstructured":"Audemard, G., Lagniez, J.M., Marquis, P.: On the computation of contrastive explanations for boosted regression trees. IOS Press (2024). https:\/\/doi.org\/10.3233\/faia240600","journal-title":"IOS Press"},{"key":"15_CR4","doi-asserted-by":"publisher","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.) NASA Formal Methods, pp. 19\u201336. Lecture Notes in Computer Science, Springer International Publishing, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-76384-8_2","DOI":"10.1007\/978-3-030-76384-8_2"},{"key":"15_CR5","doi-asserted-by":"publisher","unstructured":"Balan, R., Singh, M., Zou, D.: Lipschitz properties for deep convolutional networks (2017). https:\/\/doi.org\/10.48550\/ARXIV.1701.05217","DOI":"10.48550\/ARXIV.1701.05217"},{"key":"15_CR6","unstructured":"Balunovic, M., Baader, M., Singh, G., Gehr, T., Vechev, M.: Certifying geometric robustness of neural networks. In: Advances in Neural Information Processing Systems. vol.\u00a032. Curran Associates, Inc. (2019). https:\/\/papers.nips.cc\/paper\/2019\/hash\/f7fa6aca028e7ff4ef62d75ed025fe76-Abstract.html"},{"key":"15_CR7","doi-asserted-by":"publisher","unstructured":"Barbosa, H., et al.: cvc5: a versatile and industrial-strength SMT solver. In: Fisman, D., Rosu, G. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part I. Lecture Notes in Computer Science, vol. 13243, pp. 415\u2013442. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_24","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"15_CR8","doi-asserted-by":"publisher","unstructured":"Bassan, S., Katz, G.: Towards Formal XAI: Formally Approximate Minimal Explanations of Neural Networks, pp. 187\u2013207. Springer Nature Switzerland (2023). https:\/\/doi.org\/10.1007\/978-3-031-30823-9_10","DOI":"10.1007\/978-3-031-30823-9_10"},{"key":"15_CR9","unstructured":"Boetius, D., Leue, S.: Verifying global neural network specifications using hyperproperties (2023)"},{"key":"15_CR10","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 (2024). https:\/\/doi.org\/10.48550\/ARXIV.2412.19985, https:\/\/arxiv.org\/abs\/2412.19985","DOI":"10.48550\/ARXIV.2412.19985"},{"key":"15_CR11","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 (2023)","DOI":"10.1007\/s10009-023-00703-4"},{"key":"15_CR12","doi-asserted-by":"crossref","unstructured":"Brix, C., M\u00fcller, M.N., Bak, S., Johnson, T.T., Liu, C.: First three years of the international verification of neural networks competition (VNN-COMP) (2023)","DOI":"10.1007\/s10009-023-00703-4"},{"key":"15_CR13","doi-asserted-by":"crossref","unstructured":"Casadio, M., et al.: Neural network robustness as a verification property: a principled case study. In: International Conference on Computer Aided Verification, pp. 219\u2013231. Springer (2022)","DOI":"10.1007\/978-3-031-13185-1_11"},{"key":"15_CR14","doi-asserted-by":"publisher","unstructured":"Chareton, C., Bardin, S., Bobot, F., Perrelle, V., Valiron, B.: An Automated Deductive Verification Framework for Circuit-building Quantum Programs, pp. 148\u2013177. Springer International Publishing (2021). https:\/\/doi.org\/10.1007\/978-3-030-72019-3_6","DOI":"10.1007\/978-3-030-72019-3_6"},{"key":"15_CR15","doi-asserted-by":"publisher","unstructured":"Chen, T., Guestrin, C.: XGBoost: a scalable tree boosting system. In: Proceedings of the 22nd ACM SIGKDD International Conference on Knowledge Discovery and Data Mining, pp. 785\u2013794. KDD \u201916, ACM, New York, NY, USA (2016). https:\/\/doi.org\/10.1145\/2939672.2939785","DOI":"10.1145\/2939672.2939785"},{"key":"15_CR16","unstructured":"Conchon, S., Coquereau, A., Iguernlala, M., Mebsout, A.: Alt-Ergo 2.2. In: SMT Workshop: International Workshop on Satisfiability Modulo Theories. Oxford, United Kingdom (2018). https:\/\/hal.inria.fr\/hal-01960203"},{"key":"15_CR17","unstructured":"Conchon, S., Filli\u00e2tre, J.C., Signoles, J.: Designing a generic graph library using ML functors. In: Moraz\u00e1n, M.T., Nilsson, H. (eds.) The Eighth Symposium on Trends in Functional Programming. vol. TR-SHU-CS-2007-04-1, pp. XII\/1\u201313. Seton Hall University, New York, USA (2007). https:\/\/usr.lmf.cnrs.fr\/~jcf\/publis\/ocamlgraph-tfp07.ps"},{"key":"15_CR18","unstructured":"\u201cConfiance.ai\u201d: \u201cmethodological guideline for assessing the trustworthiness of models of artificial intelligence with caisar\u201d (2024). https:\/\/catalog.confiance.ai\/records\/wqm9q-cnv75"},{"key":"15_CR19","doi-asserted-by":"publisher","unstructured":"Cordeiro, L.C., et al.: Neural network verification is a programming language challenge (2025). https:\/\/doi.org\/10.48550\/ARXIV.2501.05867","DOI":"10.48550\/ARXIV.2501.05867"},{"key":"15_CR20","doi-asserted-by":"publisher","unstructured":"Cristianini, N., Ricci, E.: Support Vector Machines, pp. 928\u2013932. Springer US, Boston, MA (2008). https:\/\/doi.org\/10.1007\/978-0-387-30162-4_415","DOI":"10.1007\/978-0-387-30162-4_415"},{"key":"15_CR21","doi-asserted-by":"publisher","unstructured":"Daggitt, M.L., Kokke, W., Atkey, R., Arnaboldi, L., Komendantskya, E.: Vehicle: Interfacing neural network verifiers with interactive theorem provers (2022). https:\/\/doi.org\/10.48550\/ARXIV.2202.05207","DOI":"10.48550\/ARXIV.2202.05207"},{"key":"15_CR22","doi-asserted-by":"publisher","unstructured":"Daggitt, M.L., Kokke, W., Atkey, R., Slusarz, N., Arnaboldi, L., Komendantskaya, E.: Vehicle: Bridging the embedding gap in the verification of neuro-symbolic programs (2024). https:\/\/doi.org\/10.48550\/ARXIV.2401.06379","DOI":"10.48550\/ARXIV.2401.06379"},{"key":"15_CR23","doi-asserted-by":"publisher","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, pp. 337\u2013340. Lecture Notes in Computer Science, Springer, Berlin, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"15_CR24","unstructured":"Durand, S., Lemesle, A., Chihani, Z., Urban, C., Terrier, F.: ReCIPH: relational coefficients for input partitioning heuristic. WFVML 2022 (2022). https:\/\/inria.hal.science\/hal-03926281, poster"},{"key":"15_CR25","doi-asserted-by":"publisher","unstructured":"Filli\u00e2tre, J.C., Paskevich, A.: Why3 - where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) Programming Languages and Systems, pp. 125\u2013128. Lecture Notes in Computer Science, Springer, Berlin, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-37036-6_8","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"15_CR26","unstructured":"Fischer, M., Balunovic, M., Drachsler-Cohen, D., Gehr, T., Zhang, C., Vechev, M.: DL2: training and querying neural networks with logic. In: Chaudhuri, K., Salakhutdinov, R. (eds.) Proceedings of the 36th International Conference on Machine Learning. Proceedings of Machine Learning Research, vol.\u00a097, pp. 1931\u20131941. PMLR (2019). https:\/\/proceedings.mlr.press\/v97\/fischer19a.html"},{"key":"15_CR27","doi-asserted-by":"crossref","unstructured":"Girard-Satabin, J., Charpiat, G., Chihani, Z., Schoenauer, M.: CAMUS: a framework to build formal specifications for deep perception systems using simulators. In: ECAI 2020 - 24th European Conference on Artificial Intelligence. Santiago de Compostela, Spain (2020). https:\/\/hal.inria.fr\/hal-02440520","DOI":"10.3233\/FAIA200383"},{"key":"15_CR28","doi-asserted-by":"publisher","unstructured":"Katz, G., Barrett, C., Dill, D.L., Julian, K., Kochenderfer, M.J.: Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks, pp. 97\u2013117. Springer International Publishing (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_5","DOI":"10.1007\/978-3-319-63387-9_5"},{"key":"15_CR29","doi-asserted-by":"publisher","unstructured":"Katz, G., et al.: The marabou framework for verification and analysis of deep neural networks. In: Dillig, I., Tasiran, S. (eds.) Computer Aided Verification, vol. 11561, pp. 443\u2013452. Springer International Publishing, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_26","DOI":"10.1007\/978-3-030-25540-4_26"},{"key":"15_CR30","unstructured":"K\u00f6nig, M., Bosman, A.W., Hoos, H.H., van Rijn, J.N.: Critically assessing the state of the art in neural network verification. J. Mach. Learn. Res. 25(12), 1\u201353 (2024). http:\/\/jmlr.org\/papers\/v25\/23-0119.html"},{"key":"15_CR31","doi-asserted-by":"publisher","unstructured":"Lemesle, A., Lehmann, J., Gall, T.L.: Neural network verification with PyRAT (2024). https:\/\/doi.org\/10.48550\/ARXIV.2410.23903","DOI":"10.48550\/ARXIV.2410.23903"},{"key":"15_CR32","doi-asserted-by":"crossref","unstructured":"Lemesle, A., Varasse, A., Chihani, Z., Tachet, D.: AIMOS: Metamorphic Testing of AI - An Industrial Application. WAISE 2023 (2023)","DOI":"10.1007\/978-3-031-40953-0_27"},{"key":"15_CR33","doi-asserted-by":"publisher","unstructured":"Pulina, L., Tacchella, A.: NeVer: a tool for artificial neural networks verification. Ann. Math. Artif. Intell. 62(3\u20134), 403\u2013425 (2011). https:\/\/doi.org\/10.1007\/s10472-011-9243-0","DOI":"10.1007\/s10472-011-9243-0"},{"key":"15_CR34","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/978-3-030-32304-2_14","volume-title":"Static Analysis","author":"F Ranzato","year":"2019","unstructured":"Ranzato, F., Zanella, M.: Robustness verification of support vector machines. In: Chang, B.Y.E. (ed.) Static Analysis, pp. 271\u2013295. Springer International Publishing, Cham (2019)"},{"key":"15_CR35","unstructured":"Singh, G., Ganvir, R., P\u00fcschel, M., Vechev, M.: Beyond the single neuron convex barrier for neural network certification. In: Wallach, H., Larochelle, H., Beygelzimer, A., Alch\u00e9-Buc, F.d., Fox, E., Garnett, R. (eds.) Advances in Neural Information Processing Systems 32, pp. 15098\u201315109. Curran Associates, Inc. (2019). http:\/\/papers.nips.cc\/paper\/9646-beyond-the-single-neuron-convex-barrier-for-neural-network-certification.pdf"},{"key":"15_CR36","doi-asserted-by":"publisher","unstructured":"Trojanek, P., Eder, K.: Verification and testing of mobile robot navigation algorithms: a case study in spark. In: 2014 IEEE\/RSJ International Conference on Intelligent Robots and Systems, pp. 1489\u20131494. IEEE (2014). https:\/\/doi.org\/10.1109\/iros.2014.6942753","DOI":"10.1109\/iros.2014.6942753"},{"key":"15_CR37","doi-asserted-by":"crossref","unstructured":"Urban, C., Christakis, M., W\u00fcstholz, V., Zhang, F.: Perfectly Parallel Fairness Certification of Neural Networks. arXiv:1912.02499 [cs] (2019)","DOI":"10.1145\/3428253"},{"key":"15_CR38","unstructured":"Urban, C., Min\u00e9, A.: A Review of Formal Methods applied to Machine Learning. arXiv:2104.02466 [cs] (2021)"},{"key":"15_CR39","doi-asserted-by":"publisher","unstructured":"van\u00a0der Walt, S., et al.: scikit-image: image processing in Python. PeerJ 2, e453 (2014). https:\/\/doi.org\/10.7717\/peerj.453","DOI":"10.7717\/peerj.453"},{"key":"15_CR40","unstructured":"Wang, S., et al.: Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verification. http:\/\/arxiv.org\/abs\/2103.06624"},{"key":"15_CR41","doi-asserted-by":"publisher","unstructured":"Wu, H., et al.: Marabou 2.0: A versatile formal analyzer of neural networks (2024). https:\/\/doi.org\/10.48550\/ARXIV.2401.14461","DOI":"10.48550\/ARXIV.2401.14461"},{"key":"15_CR42","unstructured":"Wu, M., Wu, H., Barrett, C.: VeriX: Towards verified explainability of deep neural networks (2023)"},{"key":"15_CR43","doi-asserted-by":"publisher","unstructured":"Xie, X., Kersting, K., Neider, D.: Neuro-symbolic verification of deep neural networks. In: Raedt, L.D. (ed.) Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence, IJCAI-22, pp. 3622\u20133628. International Joint Conferences on Artificial Intelligence Organization (2022). https:\/\/doi.org\/10.24963\/ijcai.2022\/503, main Track","DOI":"10.24963\/ijcai.2022\/503"}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-10794-7_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T13:59:27Z","timestamp":1767967167000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-10794-7_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,16]]},"ISBN":["9783032107930","9783032107947"],"references-count":43,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-10794-7_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,11,16]]},"assertion":[{"value":"16 November 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"IFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Integrated Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Paris","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":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19 November 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 November 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ifm2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/ifm2025.ens.psl.eu\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}