{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T09:06:18Z","timestamp":1784797578045,"version":"3.55.0"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032325259","type":"print"},{"value":"9783032325266","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:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,7,24]],"date-time":"2026-07-24T00:00:00Z","timestamp":1784851200000},"content-version":"vor","delay-in-days":204,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    Research on neural network verification has traditionally emphasized scalability. However, recent invalidations of formally verified results of neural networks highlight\n                    <jats:italic>soundness<\/jats:italic>\n                    as an equally important goal. Pursuing inherent soundness, we present\n                    <jats:italic>Rocq-NN-Roll<\/jats:italic>\n                    , the first\n                    <jats:italic>formally verified<\/jats:italic>\n                    prover for rational-valued piecewise-affine neural networks. Rocq-NN-Roll combines a network and its specification, including hyperproperties, into a piecewise-affine function and reduces the verification task to solving linear inequalities over the network\u2019s polyhedral regions. Developed in Rocq, the prover also provides the first automated proof support for neural networks within any interactive theorem prover, highlighting their still underexplored role in this field.\n                  <\/jats:p>","DOI":"10.1007\/978-3-032-32526-6_23","type":"book-chapter","created":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T08:46:01Z","timestamp":1784796361000},"page":"480-503","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["The Rocq-NN-Roll Prover: Soundly Verifying Hyperproperties of Neural Networks in Rocq"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4717-4206","authenticated-orcid":false,"given":"Andrei","family":"Aleksandrov","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Malte","family":"Jackisch","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Kim","family":"V\u00f6llinger","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,7,24]]},"reference":[{"key":"23_CR1","doi-asserted-by":"publisher","unstructured":"Albarghouthi, A.: Introduction to Neural Network Verification. Found. Trends Program. Lang. 7(1\u20132), 1\u2013157 (dec 2021). https:\/\/doi.org\/10.1561\/2500000051","DOI":"10.1561\/2500000051"},{"key":"23_CR2","doi-asserted-by":"publisher","unstructured":"Aleksandrov, A., V\u00f6llinger, K.: Formalizing piecewise affine activation functions of neural networks in Coq. In: 15th International Symposium, Nasa Formal Methods 2023, Houston, TX, USA (2023). https:\/\/doi.org\/10.1007\/978-3-031-33170-1_4","DOI":"10.1007\/978-3-031-33170-1_4"},{"key":"23_CR3","doi-asserted-by":"publisher","unstructured":"Allamigeon, X., Katz, R.D.: A formalization of convex polyhedra based on the simplex method. J. Autom. Reason. 63(2), 323\u2013345 (2019). https:\/\/doi.org\/10.1007\/s10817-018-9477-1","DOI":"10.1007\/s10817-018-9477-1"},{"key":"23_CR4","doi-asserted-by":"publisher","unstructured":"Apt, K.: Some complete constraint solvers, p. 82\u2013134. Cambridge University Press (2003). https:\/\/doi.org\/10.1017\/CBO9780511615320.004","DOI":"10.1017\/CBO9780511615320.004"},{"key":"23_CR5","doi-asserted-by":"publisher","unstructured":"Bagnall, A., Stewart, G.: Certifying the true error: machine learning in Coq with verified generalization guarantees. In: AAAI Conference on Artificial Intelligence, (2019). https:\/\/doi.org\/10.1609\/aaai.v33i01.33012662","DOI":"10.1609\/aaai.v33i01.33012662"},{"key":"23_CR6","doi-asserted-by":"publisher","unstructured":"Boetius, D., Leue, S.: Verifying global neural network specifications using hyperproperties. In: Narodytska, N., Amir, G., Katz, G., Isac, O. (eds.) Proceedings of the 6th Workshop on Formal Methods for ML-Enabled Autonomous Systems, FoMLAS@CAV 2023, Paris, France, July 17-18, 2023, pp. 71\u201382. Kalpa Publications in Computing, EasyChair (2023). https:\/\/doi.org\/10.29007\/PVTN","DOI":"10.29007\/PVTN"},{"issue":"1","key":"23_CR7","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/s11786-014-0181-1","volume":"9","author":"S Boldo","year":"2015","unstructured":"Boldo, S., Lelay, C., Melquiond, G.: Coquelicot: a user-friendly library of real analysis for Coq. Math. Comput. Sci. 9(1), 41\u201362 (2015). https:\/\/doi.org\/10.1007\/s11786-014-0181-1","journal-title":"Math. Comput. Sci."},{"key":"23_CR8","doi-asserted-by":"publisher","unstructured":"Boldo, S., Melquiond, G.: Flocq: A unified library for proving floating-point algorithms in coq. In: IEEE 20th Symposium on Computer Arithmetic, pp. 243\u2013252. IEEE (2011). https:\/\/doi.org\/10.1109\/ARITH.2011.40","DOI":"10.1109\/ARITH.2011.40"},{"issue":"4","key":"23_CR9","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3617508","volume":"23","author":"F Boudardara","year":"2024","unstructured":"Boudardara, F., Boussif, A., Meyer, P.J., Ghazel, M.: A review of abstraction methods toward verifying neural networks. ACM Trans. Embedded Comput. Syst. 23(4), 1\u201319 (2024). https:\/\/doi.org\/10.1145\/3617508","journal-title":"ACM Trans. Embedded Comput. Syst."},{"key":"23_CR10","doi-asserted-by":"publisher","unstructured":"Brucker, A.D., Stell, A.: Verifying feedforward neural networks for classification in Isabelle\/HOL. In: Proceedings of the 25th International Symposium on Formal Methods. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-27481-7_24","DOI":"10.1007\/978-3-031-27481-7_24"},{"key":"23_CR11","unstructured":"Bunel, R., Turkaslan, I., Torr, P.H., Kohli, P., Kumar, M.P.: A Unified View of Piecewise Linear Neural Network Verification. In: Proceedings of the 32nd International Conference on Neural Information Processing Systems, pp. 4795\u20134804. NIPS\u201918, Curran Associates Inc., Red Hook, NY, USA (2018). https:\/\/proceedings.neurips.cc\/paper_files\/paper\/2018\/file\/be53d253d6bc3258a8160556dda3e9b2-Paper.pdf"},{"key":"23_CR12","doi-asserted-by":"publisher","unstructured":"Clarkson, M.R., Schneider, F.B.: Hyperproperties. In: Proceedings of the 2008 21st IEEE Computer Security Foundations Symposium, pp. 51\u201365. CSF \u201908, IEEE Computer Society, USA (2008). https:\/\/doi.org\/10.1109\/CSF.2008.7","DOI":"10.1109\/CSF.2008.7"},{"key":"23_CR13","doi-asserted-by":"publisher","unstructured":"Cordeiro, L.C., et\u00a0al.: Neural network verification is a programming language challenge. In: European Symposium on Programming, pp. 206\u2013235. Springer (2025). https:\/\/doi.org\/10.1007\/978-3-031-91118-7_9","DOI":"10.1007\/978-3-031-91118-7_9"},{"key":"23_CR14","doi-asserted-by":"publisher","unstructured":"Demarchi, S., Guidotti, D., Pulina, L., Tacchella, A.: Supporting standardization of neural networks verification with VNNLIB and coconet. In: Narodytska, N., Amir, G., Katz, G., Isac, O. (eds.) Proceedings of the 6th Workshop on Formal Methods for ML-Enabled Autonomous Systems, FoMLAS@CAV 2023, Paris, France, July 17-18, 2023, pp. 47\u201358. Kalpa Publications in Computing, EasyChair (2023). https:\/\/doi.org\/10.29007\/5PDH","DOI":"10.29007\/5PDH"},{"key":"23_CR15","doi-asserted-by":"publisher","unstructured":"Desmartin, R., Isac, O., Passmore, G., Komendantskaya, E., Stark, K., Katz, G.: A certified proof checker for deep neural network verification in Imandra. In: Forster, Y., Keller, C. (eds.) 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0352, pp. 1:1\u20131:21. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2025). https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2025.1","DOI":"10.4230\/LIPIcs.ITP.2025.1"},{"key":"23_CR16","doi-asserted-by":"publisher","unstructured":"Desmartin, R., et al.: Neural networks in imandra: Matrix representation as a verification choice. Presented at the (2022). https:\/\/doi.org\/10.1007\/978-3-031-21222-2_6 Software Verification and Formal Methods for ML-Enabled Autonomous Systems","DOI":"10.1007\/978-3-031-21222-2_6"},{"key":"23_CR17","doi-asserted-by":"publisher","unstructured":"Ducoffe, M., Gabreau, C., Ober, I., Ober, I., Vidot, E.G.: Certification of avionic software based on machine learning: the case for formal monotony analysis. Int. J. Softw. Tools Technol. Transfer 26(2), 189\u2013205 (2024). https:\/\/doi.org\/10.1007\/s10009-024-00741-6","DOI":"10.1007\/s10009-024-00741-6"},{"key":"23_CR18","doi-asserted-by":"publisher","unstructured":"George, R.J., Cruden, J., Zhong, X., Zhang, H., Anandkumar, A.: TorchLean: Formalizing Neural Networks in Lean. https:\/\/doi.org\/10.48550\/arXiv.2602.22631. https:\/\/doi.org\/10.48550\/arXiv.2602.22631","DOI":"10.48550\/arXiv.2602.22631"},{"key":"23_CR19","doi-asserted-by":"publisher","unstructured":"Gummersbach, L.A., V\u00f6llinger, K., Aleksandrov, A.: A formally verified neural network converter for the interactive theorem prover Coq. In: The 19th International Symposium on Theoretical Aspects of Software Engineering, Springer (2025). https:\/\/doi.org\/10.1007\/978-3-031-98208-8_12","DOI":"10.1007\/978-3-031-98208-8_12"},{"key":"23_CR20","doi-asserted-by":"publisher","unstructured":"Huchette, J., Mu\u00f1oz, G., Serra, T., Tsay, C.: When deep learning meets polyhedral theory: a survey. INFORMS J. Comput. 0(0) (2026). https:\/\/doi.org\/10.1287\/ijoc.2024.0902","DOI":"10.1287\/ijoc.2024.0902"},{"key":"23_CR21","doi-asserted-by":"publisher","unstructured":"Jia, K., Rinard, M.: Exploiting verified neural networks via floating point numerical error. In: International Static Analysis Symposium, pp. 191\u2013205. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-88806-0_9","DOI":"10.1007\/978-3-030-88806-0_9"},{"key":"23_CR22","unstructured":"Jordan, M., Lewis, J., Dimakis, A.G.: Provable certificates for adversarial examples: Fitting a ball in the union of polytopes. Adv. Neural Inform. Process. Syst. 32 (2019). https:\/\/proceedings.neurips.cc\/paper_files\/paper\/2019\/file\/ae3f4c649fb55c2ee3ef4d1abdb79ce5-Paper.pdf"},{"key":"23_CR23","doi-asserted-by":"publisher","unstructured":"Leroy, X.: Formal certification of a compiler back-end or: programming a compiler with a proof assistant. SIGPLAN Not. 41(1), 42\u201354 (Jan 2006). https:\/\/doi.org\/10.1145\/1111320.1111042","DOI":"10.1145\/1111320.1111042"},{"key":"23_CR24","doi-asserted-by":"publisher","unstructured":"Loulergue, F., Ed-Dbali, A.: Verified high performance computing: The sydpacc approach. In: International Conference on Verification and Evaluation of Computer and Communication Systems, pp. 15\u201329. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-49737-7_2","DOI":"10.1007\/978-3-031-49737-7_2"},{"key":"23_CR25","doi-asserted-by":"publisher","unstructured":"Montesinos\u00a0L\u00f3pez, O.A., Montesinos\u00a0L\u00f3pez, A., Crossa, J.: Fundamentals of artificial neural networks and deep learning. In: Multivariate Statistical Machine Learning Methods for Genomic Prediction, pp. 379\u2013425. Springer International Publishing (2022). https:\/\/doi.org\/10.1007\/978-3-030-89010-0_10","DOI":"10.1007\/978-3-030-89010-0_10"},{"key":"23_CR26","doi-asserted-by":"publisher","unstructured":"Pulina, L., Tacchella, A.: Checking safety of neural networks with SMT solvers: a comparative evaluation. In: Congress of the Italian Association for Artificial Intelligence, pp. 127\u2013138. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-23954-0_14","DOI":"10.1007\/978-3-642-23954-0_14"},{"key":"23_CR27","doi-asserted-by":"publisher","unstructured":"Rocq: The Rocq Prover. https:\/\/rocq-prover.org\/https:\/\/doi.org\/10.5281\/zenodo.15149628","DOI":"10.5281\/zenodo.15149628"},{"key":"23_CR28","doi-asserted-by":"publisher","unstructured":"\u0160inkarovs, A.: Multi-dimensional arrays with levels. In: New, M.S., Lindley, S. (eds.) Proceedings Eighth Workshop on Mathematically Structured Functional Programming, MSFP@ETAPS 2020, Dublin, Ireland, 25th April 2020. EPTCS, vol.\u00a0317, pp. 57\u201371 (2020). https:\/\/doi.org\/10.4204\/EPTCS.317.4","DOI":"10.4204\/EPTCS.317.4"},{"key":"23_CR29","doi-asserted-by":"publisher","unstructured":"Sinkarovs, A., Koopman, T., Scholz, S.B.: Correctness is demanding, performance is frustrating (2024). https:\/\/doi.org\/10.48550\/arXiv.2406.10405","DOI":"10.48550\/arXiv.2406.10405"},{"key":"23_CR30","unstructured":"Sz\u00e1sz, A., B\u00e1nhelyi, B., Jelasity, M.: No soundness in the real world: on the challenges of the verification of deployed neural networks 267, 58088\u201358105 (13\u201319 Jul 2025). https:\/\/proceedings.mlr.press\/v267\/szasz25a.html"},{"key":"23_CR31","doi-asserted-by":"publisher","unstructured":"Tobler, J., Syeda, H.T., Murray, T.: A formally verified robustness certifier for neural networks. In: Piskac, R., Rakamari\u0107, Z. (eds.) Computer Aided Verification, pp. 327\u2013348. Springer Nature Switzerland, Cham (2025). https:\/\/doi.org\/10.1007\/978-3-031-98679-6_15","DOI":"10.1007\/978-3-031-98679-6_15"},{"key":"23_CR32","doi-asserted-by":"publisher","unstructured":"Vincent, J.A., Schwager, M.: Reachable polyhedral marching (rpm): an exact analysis tool for deep-learned control systems. IEEE Trans. Neural Netw. Learn. Syst. (2025). https:\/\/doi.org\/10.1109\/TNNLS.2025.3571720","DOI":"10.1109\/TNNLS.2025.3571720"},{"key":"23_CR33","unstructured":"Zhou, D., Chavez, J., Chen, H., Hanasusanto, G.A., Zhang, H.: Clip-and-verify: Linear constraint-driven domain clipping for accelerating neural network verification 38, 174849\u2013174895 (2025). https:\/\/proceedings.neurips.cc\/paper_files\/paper\/2025\/file\/ffa977364ab7046c803da0e04dbb2832-Paper-Conference.pdf"}],"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-032-32526-6_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T08:46:05Z","timestamp":1784796365000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-32526-6_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032325259","9783032325266"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-32526-6_23","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":"24 July 2026","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","label":"Disclosure of Interests","group":{"name":"EthicsHeading","label":"Ethics"}},{"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":"Lisbon","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","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":"26 July 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 July 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"38","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.floc26.org\/program","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}