{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,3,22]],"date-time":"2024-03-22T01:00:50Z","timestamp":1711069250051},"reference-count":44,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2024,3,12]],"date-time":"2024-03-12T00:00:00Z","timestamp":1710201600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,3,12]],"date-time":"2024-03-12T00:00:00Z","timestamp":1710201600000},"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":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2024,4]]},"DOI":"10.1007\/s10009-024-00741-6","type":"journal-article","created":{"date-parts":[[2024,3,12]],"date-time":"2024-03-12T22:01:51Z","timestamp":1710280911000},"page":"189-205","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Certification of avionic software based on machine learning: the case for formal monotony analysis"],"prefix":"10.1007","volume":"26","author":[{"given":"M\u00e9lanie","family":"Ducoffe","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christophe","family":"Gabreau","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ileana","family":"Ober","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Iulian","family":"Ober","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Eric Guillaume","family":"Vidot","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,3,12]]},"reference":[{"key":"741_CR1","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1109\/ICSE-SEIP.2019.00042","volume-title":"2019 IEEE\/ACM 41st International Conference on Software Engineering: Software Engineering in Practice (ICSE-SEIP)","author":"S. Amershi","year":"2019","unstructured":"Amershi, S., Begel, A., Bird, C., et al.: Software engineering for machine learning: a case study. In: 2019 IEEE\/ACM 41st International Conference on Software Engineering: Software Engineering in Practice (ICSE-SEIP), pp.\u00a0291\u2013300 (2019). https:\/\/doi.org\/10.1109\/ICSE-SEIP.2019.00042"},{"key":"741_CR2","volume":"12","author":"J. Biannic","year":"2016","unstructured":"Biannic, J., Hardier, G., Roos, C., et al.: Surrogate models for aircraft flight control: some off-line and embedded applications. Aerosp. Lab. 12, 1 (2016)","journal-title":"Aerosp. Lab."},{"key":"741_CR3","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1109\/SP.2017.49","volume-title":"IEEE SP. IEEE Computer Society","author":"N. Carlini","year":"2017","unstructured":"Carlini, N., Wagner, D.A.: Towards evaluating the robustness of neural networks. In: IEEE SP. IEEE Computer Society, pp.\u00a039\u201357 (2017). https:\/\/doi.org\/10.1109\/SP.2017.49"},{"key":"741_CR4","doi-asserted-by":"publisher","first-page":"8978","DOI":"10.1109\/ICRA46639.2022.9812177","volume-title":"2022 International Conference on Robotics and Automation (ICRA)","author":"S. Chen","year":"2022","unstructured":"Chen, S., Sun, Y., Li, D., et al.: Runtime safety assurance for learning-enabled control of autonomous driving vehicles. In: 2022 International Conference on Robotics and Automation (ICRA), pp.\u00a08978\u20138984 (2022). https:\/\/doi.org\/10.1109\/ICRA46639.2022.9812177"},{"key":"741_CR5","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/978-3-319-68167-2_18","volume-title":"Automated Technology for Verification and Analysis","author":"C.H. Cheng","year":"2017","unstructured":"Cheng, C.H., N\u00fchrenberg, G., Ruess, H.: Maximum resilience of artificial neural networks. In: D\u2019Souza, D., Narayan Kumar, K. (eds.) Automated Technology for Verification and Analysis, pp.\u00a0251\u2013268. Springer, Berlin (2017). https:\/\/doi.org\/10.1007\/978-3-319-68167-2_18"},{"key":"741_CR6","series-title":"Proceedings, Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1007\/978-3-030-55754-6_21","volume-title":"NASA Formal Methods \u2013 12th International Symposium, NFM 2020","author":"D.D. Cofer","year":"2020","unstructured":"Cofer, D.D., Amundson, I., Sattigeri, R., et al.: Run-time assurance for learning-enabled systems. In: Lee, R., Jha, S., Mavridou, A. (eds.) NASA Formal Methods \u2013 12th International Symposium, NFM 2020, Moffett Field, CA, USA, May 11\u201315, 2020. Proceedings, Lecture Notes in Computer Science, vol.\u00a012229, pp.\u00a0361\u2013368. Springer, Berlin (2020). https:\/\/doi.org\/10.1007\/978-3-030-55754-6_21"},{"key":"741_CR7","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1007\/978-3-030-83903-1_3","volume-title":"Proceedings","author":"M. Damour","year":"2021","unstructured":"Damour, M., Grancey, F.D., Gabreau, C., et al.: Towards certification of a reduced footprint ACAS-Xu system: a hybrid L-based solution. In: Proceedings, Computer Safety, Reliability, and Security \u2013 40th International Conference,SAFECOMP 2021, York, UK, September 8-10, 2021, pp.\u00a034\u201348 (2021). https:\/\/doi.org\/10.1007\/978-3-030-83903-1_3"},{"key":"741_CR8","series-title":"Proceedings, 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, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008","author":"L.M. de Moura","year":"2008","unstructured":"de Moura, L.M., Bj\u00f8rner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008. Budapest, Hungary, March 29-April 6, 2008. Proceedings, Lecture Notes in Computer Science, vol.\u00a04963, pp.\u00a0337\u2013340. Springer, Berlin (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"741_CR9","unstructured":"EASA: CS-25 Amendment 27 (2021). https:\/\/www.easa.Europa.eu\/downloads\/136622\/en"},{"key":"741_CR10","unstructured":"EASA: EASA Concept Paper: First usable guidance for Level 1 machine learning applications (2021). https:\/\/www.easa.Europa.eu\/downloads\/134357\/en"},{"key":"741_CR11","doi-asserted-by":"publisher","first-page":"395","DOI":"10.1007\/3-540-45372-5_42","volume-title":"European Conference on Principles of Data Mining and Knowledge Discovery","author":"A.J. Feelders","year":"2000","unstructured":"Feelders, A.J.: Prior knowledge in economic applications of data mining. In: European Conference on Principles of Data Mining and Knowledge Discovery, pp.\u00a0395\u2013400. Springer, Berlin (2000). https:\/\/doi.org\/10.1007\/3-540-45372-5_42"},{"key":"741_CR12","unstructured":"Gauffriau, A., Malgouyres, F., Ducoffe, M.: Overestimation learning with guarantees (2021). arXiv preprint arXiv:2101.11717"},{"key":"741_CR13","unstructured":"Grossmann, I.E.: Review of nonlinear mixed-integer and disjunctive programming techniques. Optim. Eng. (2002)"},{"key":"741_CR14","unstructured":"Gupta, A., Shukla, N., Marla, L., et\u00a0al.: How to incorporate monotonicity in deep networks while preserving flexibility? (2019). arXiv preprint arXiv:1909.10662"},{"key":"741_CR15","unstructured":"Gurobi Optimization, LLC: Gurobi Optimizer Reference Manual (2022). https:\/\/www.gurobi.com"},{"key":"741_CR16","doi-asserted-by":"publisher","DOI":"10.1016\/j.aei.2021.101342","volume":"49","author":"J. Hao","year":"2021","unstructured":"Hao, J., Ye, W., Jia, L., et al.: Building surrogate models for engineering problems by integrating limited simulation data and monotonic engineering knowledge. Adv. Eng. Inform. 49, 101342 (2021). https:\/\/doi.org\/10.1016\/j.aei.2021.101342","journal-title":"Adv. Eng. Inform."},{"key":"741_CR17","doi-asserted-by":"publisher","DOI":"10.5220\/0006418100830092","volume-title":"SIMULTECH 2017: Proceedings of the 7th International Conference on Simulation and Modeling Methodologies, Technologies and Applications. SCITEPRESS","author":"Z.D. Jian","year":"2017","unstructured":"Jian, Z.D., Chang, H.J., Ts, H., et al.: Learning from simulated world \u2013 surrogates construction with deep neural network. In: SIMULTECH 2017: Proceedings of the 7th International Conference on Simulation and Modeling Methodologies, Technologies and Applications. SCITEPRESS (2017). https:\/\/doi.org\/10.5220\/0006418100830092"},{"key":"741_CR18","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1145\/112646.112684","volume-title":"Proceedings of the 3rd International Conference on Artificial Intelligence and Law","author":"J. Karpf","year":"1991","unstructured":"Karpf, J.: Inductive modelling in law: example based expert systems in administrative law. In: Proceedings of the 3rd International Conference on Artificial Intelligence and Law, pp.\u00a0297\u2013306 (1991). https:\/\/doi.org\/10.1145\/112646.112684"},{"key":"741_CR19","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1007\/978-3-030-25540-4_26","volume-title":"Computer Aided Verification","author":"G. Katz","year":"2019","unstructured":"Katz, G., Huang, D.A., Ibeling, D., et al.: The marabou framework for verification and analysis of deep neural networks. In: Dillig, I., Tasiran, S. (eds.) Computer Aided Verification, pp.\u00a0443\u2013452. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_26"},{"key":"741_CR20","first-page":"15427","volume":"33","author":"X. Liu","year":"2020","unstructured":"Liu, X., Han, X., Zhang, N., et al.: Certified monotonic neural networks. Adv. Neural Inf. Process. Syst. 33, 15427\u201315438 (2020). https:\/\/proceedings.neurips.cc\/paper\/2020\/hash\/b139aeda1c2914e3b579aafd3ceeb1bd-Abstract.html","journal-title":"Adv. Neural Inf. Process. Syst."},{"key":"741_CR21","unstructured":"Madry, A., Makelov, A., Schmidt, L., et\u00a0al.: Towards deep learning models resistant to adversarial attacks. In: ICLR. OpenReview.net (2018). https:\/\/openreview.net\/forum?id=rJzIBfZAb"},{"key":"741_CR22","unstructured":"Mamalet, F., Jenn, E., Flandin, G., et\u00a0al.: White Paper Machine Learning in Certified Systems (2021). https:\/\/hal.archives-ouvertes.fr\/hal-03176080"},{"key":"741_CR23","doi-asserted-by":"crossref","unstructured":"Marques-Silva, J., Ignatiev, A.: Delivering trustworthy AI through formal XAI. In: Thirty-Sixth AAAI Conference on Artificial Intelligence, AAAI 2022, Thirty-Fourth Conference on Innovative Applications of Artificial Intelligence, IAAI 2022, The Twelveth Symposium on Educational Advances in Artificial Intelligence, EAAI 2022 Virtual Event, February 22 \u2013 March 1, 2022, pp.\u00a012342\u201312350. AAAI Press, Menlo Park (2022). https:\/\/ojs.aaai.org\/index.php\/AAAI\/article\/view\/21499","DOI":"10.1609\/aaai.v36i11.21499"},{"key":"741_CR24","unstructured":"Martin, R.: Assured software \u2013 a journey and discussion (2017). https:\/\/www.his-2019.co.uk\/session\/cwe-cve-its-history-and-future"},{"issue":"POPL","key":"741_CR25","doi-asserted-by":"publisher","DOI":"10.1145\/3498704","volume":"6","author":"M.N. M\u00fcller","year":"2022","unstructured":"M\u00fcller, M.N., Makarchuk, G., Singh, G., et al.: PRIMA: general and precise neural network certification via scalable convex hull approximations. Proc. ACM Program. Lang. 6(POPL), 43 (2022). https:\/\/doi.org\/10.1145\/3498704","journal-title":"Proc. ACM Program. Lang."},{"key":"741_CR26","unstructured":"Nguyen, A., Mart\u00ednez, M.R.: MonoNet: towards interpretable models by learning monotonic features (2019). arXiv preprint arXiv:1909.13611"},{"key":"741_CR27","doi-asserted-by":"publisher","unstructured":"Phillips, P.J., Hahn, C., Fontana, P., et\u00a0al.: Four principles of explainable artificial intelligence (2021). https:\/\/doi.org\/10.6028\/NIST.IR.8312. https:\/\/tsapps.nist.gov\/publication\/get_pdf.cfm?pub_id=933399","DOI":"10.6028\/NIST.IR.8312"},{"key":"741_CR28","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1109\/ISSREW51248.2020.00085","volume-title":"ISSRE","author":"S. Picard","year":"2020","unstructured":"Picard, S., Chapdelaine, C., Cappi, C., et al.: Ensuring dataset quality for machine learning certification. In: ISSRE, pp.\u00a0275\u2013282 (2020). https:\/\/doi.org\/10.1109\/ISSREW51248.2020.00085"},{"key":"741_CR29","first-page":"10877","volume-title":"Advances in Neural Information Processing Systems","author":"A. Raghunathan","year":"2018","unstructured":"Raghunathan, A., Steinhardt, J., Liang, P.S.: Semidefinite relaxations for certifying robustness to adversarial examples. In: Advances in Neural Information Processing Systems, pp.\u00a010877\u201310887 (2018). https:\/\/proceedings.neurips.cc\/paper\/2018\/hash\/29c0605a3bab4229e46723f89cf59d83-Abstract.html"},{"key":"741_CR30","unstructured":"Rushby, J.: The interpretation and evaluation of assurance cases. Tech. Rep., (2015) http:\/\/www.csl.sri.com\/users\/rushby\/papers\/sri-csl-15-1-assurance-cases.pdf"},{"key":"741_CR31","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1109\/DASC52595.2021.9594364","volume-title":"2021 IEEE\/AIAA 40th Digital Avionics Systems Conference (DASC)","author":"A. Schweiger","year":"2021","unstructured":"Schweiger, A., Annighoefer, B., Reich, M., et al.: Classification for avionics capabilities enabled by artificial intelligence. In: 2021 IEEE\/AIAA 40th Digital Avionics Systems Conference (DASC), pp.\u00a01\u201310 (2021). https:\/\/doi.org\/10.1109\/DASC52595.2021.9594364"},{"key":"741_CR32","volume-title":"International Conference on Learning Representations","author":"G. Singh","year":"2019","unstructured":"Singh, G., Gehr, T., P\u00fcschel, M., et al.: Robustness certification with refinement. In: International Conference on Learning Representations (2019). https:\/\/openreview.net\/forum?id=HJgeEh09KQ"},{"key":"741_CR33","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/978-3-030-22808-8_24","volume-title":"International Symposium on Neural Networks","author":"O. Sudakov","year":"2019","unstructured":"Sudakov, O., Koroteev, D., Belozerov, B., et al.: Artificial neural network surrogate modeling of oil reservoir: a case study. In: International Symposium on Neural Networks, pp.\u00a0232\u2013241. Springer, Berlin (2019). https:\/\/doi.org\/10.1007\/978-3-030-22808-8_24"},{"key":"741_CR34","volume-title":"ICLR","author":"V. Tjeng","year":"2019","unstructured":"Tjeng, V., Xiao, K.Y., Tedrake, R.: Evaluating robustness of neural networks with mixed integer programming. In: ICLR (2019). https:\/\/openreview.net\/forum?id=HyGIdiRqtm"},{"key":"741_CR35","first-page":"6542","volume-title":"NeurIPS","author":"Y. Tsuzuku","year":"2018","unstructured":"Tsuzuku, Y., Sato, I., Sugiyama, M.: Lipschitz-margin training: scalable certification of perturbation invariance for deep neural networks. In: NeurIPS, pp.\u00a06542\u20136551 (2018). https:\/\/proceedings.neurips.cc\/paper\/2018\/hash\/485843481a7edacbfce101ecb1e4d2a8-Abstract.html"},{"key":"741_CR36","unstructured":"Urban, C., Min\u00e9, A.: A review of formal methods applied to machine learning (2021). arXiv preprint arXiv:2104.02466. https:\/\/arxiv.org\/abs\/2104.02466"},{"issue":"OOPSLA","key":"741_CR37","doi-asserted-by":"publisher","DOI":"10.1145\/3428253","volume":"4","author":"C. Urban","year":"2020","unstructured":"Urban, C., Christakis, M., W\u00fcstholz, V., et al.: Perfectly parallel fairness certification of neural networks. Proc. ACM Program. Lang. 4(OOPSLA), 185 (2020). https:\/\/doi.org\/10.1145\/3428253","journal-title":"Proc. ACM Program. Lang."},{"key":"741_CR38","first-page":"1599","volume-title":"27th USENIX Security Symposium (USENIX Security","author":"S. Wang","year":"2018","unstructured":"Wang, S., Pei, K., Whitehouse, J., et al.: Formal security analysis of neural networks using symbolic intervals. In: 27th USENIX Security Symposium (USENIX Security, vol.\u00a018, pp.\u00a01599\u20131614. USENIX Association, Baltimore (2018). https:\/\/www.usenix.org\/conference\/usenixsecurity18\/presentation\/wang-shiqi"},{"key":"741_CR39","volume-title":"Advances in Neural Information Processing Systems","author":"S. Wang","year":"2021","unstructured":"Wang, S., Zhang, H., Xu, K., et al.: Beta-CROWN: efficient bound propagation with per-neuron split constraints for neural network robustness verification. In: Advances in Neural Information Processing Systems (2021). https:\/\/proceedings.neurips.cc\/paper\/2021\/hash\/fac7fead96dafceaf80c1daffeae82a4-Abstract.html"},{"key":"741_CR40","series-title":"Proceedings of Machine Learning Research","volume-title":"ICML","author":"T. Weng","year":"2018","unstructured":"Weng, T., Zhang, H., Chen, H., et al.: Towards fast computation of certified robustness for relu networks. In: ICML. Proceedings of Machine Learning Research (2018). http:\/\/proceedings.mlr.press\/v80\/weng18a.html"},{"issue":"11","key":"741_CR41","doi-asserted-by":"publisher","first-page":"5777","DOI":"10.1109\/TNNLS.2018.2808470","volume":"29","author":"W. Xiang","year":"2018","unstructured":"Xiang, W., Tran, H.D., Johnson, T.T.: Output reachable set estimation and verification for multilayer neural networks. IEEE Trans. Neural Netw. Learn. Syst. 29(11), 5777\u20135783 (2018). https:\/\/doi.org\/10.1109\/TNNLS.2018.2808470","journal-title":"IEEE Trans. Neural Netw. Learn. Syst."},{"key":"741_CR42","first-page":"1129","volume-title":"NeurIPS","author":"K. Xu","year":"2020","unstructured":"Xu, K., Shi, Z., Zhang, H., et al.: Automatic perturbation analysis for scalable certified robustness and beyond. In: NeurIPS, pp.\u00a01129\u20131141 (2020). https:\/\/proceedings.neurips.cc\/paper\/2020\/hash\/0cbc5671ae26f67871cb914d81ef8fc1-Abstract.html"},{"key":"741_CR43","first-page":"4939","volume-title":"Advances in Neural Information Processing Systems","author":"H. Zhang","year":"2018","unstructured":"Zhang, H., Weng, T.W., Chen, P.Y., et al.: Efficient neural network robustness certification with general activation functions. In: Advances in Neural Information Processing Systems, pp.\u00a04939\u20134948 (2018). https:\/\/proceedings.neurips.cc\/paper\/2018\/hash\/d04863f100d59b3eb688a11f95b0ae60-Abstract.html"},{"key":"741_CR44","doi-asserted-by":"publisher","first-page":"5757","DOI":"10.1609\/aaai.v33i01.33015757","volume-title":"Proceedings of the AAAI Conference on Artificial Intelligence","author":"H. Zhang","year":"2019","unstructured":"Zhang, H., Zhang, P., Hsieh, C.J.: Recurjac: an efficient recursive algorithm for bounding Jacobian matrix of neural networks and its applications. In: Proceedings of the AAAI Conference on Artificial Intelligence, pp.\u00a05757\u20135764 (2019). https:\/\/doi.org\/10.1609\/aaai.v33i01.33015757"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-024-00741-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10009-024-00741-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-024-00741-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,21]],"date-time":"2024-03-21T15:06:46Z","timestamp":1711033606000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10009-024-00741-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,3,12]]},"references-count":44,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2024,4]]}},"alternative-id":["741"],"URL":"https:\/\/doi.org\/10.1007\/s10009-024-00741-6","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,3,12]]},"assertion":[{"value":"6 February 2024","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"12 March 2024","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}