{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T14:34:21Z","timestamp":1742913261988,"version":"3.40.3"},"publisher-location":"Cham","reference-count":40,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783031172434"},{"type":"electronic","value":"9783031172441"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"DOI":"10.1007\/978-3-031-17244-1_1","type":"book-chapter","created":{"date-parts":[[2022,10,9]],"date-time":"2022-10-09T19:33:23Z","timestamp":1665344003000},"page":"1-19","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Bridging Formal Methods and\u00a0Machine Learning with\u00a0Global Optimisation"],"prefix":"10.1007","author":[{"given":"Xiaowei","family":"Huang","sequence":"first","affiliation":[]},{"given":"Wenjie","family":"Ruan","sequence":"additional","affiliation":[]},{"given":"Qiyi","family":"Tang","sequence":"additional","affiliation":[]},{"given":"Xingyu","family":"Zhao","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,10,10]]},"reference":[{"key":"1_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1007\/978-3-030-88494-9_18","volume-title":"Runtime Verification","author":"A Balakrishnan","year":"2021","unstructured":"Balakrishnan, A., Deshmukh, J., Hoxha, B., Yamaguchi, T., Fainekos, G.: PerceMon: online monitoring for\u00a0perception systems. In: Feng, L., Fisman, D. (eds.) RV 2021. LNCS, vol. 12974, pp. 297\u2013308. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-88494-9_18"},{"doi-asserted-by":"crossref","unstructured":"Balakrishnan, A., et al.: Specifying and evaluating quality metrics for vision-based perception systems. In: Design, Automation & Test in Europe Conference & Exhibition (DATE), pp. 1433\u20131438 (2019)","key":"1_CR2","DOI":"10.23919\/DATE.2019.8715114"},{"key":"1_CR3","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69061-0","volume-title":"Verification of Object-Oriented Software. The KeY Approach - Foreword by K. Rustan M. Leino","year":"2007","unstructured":"Beckert, B., H\u00e4hnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software. The KeY Approach - Foreword by K. Rustan M. Leino. LNCS (LNAI), vol. 4334. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-69061-0"},{"doi-asserted-by":"crossref","unstructured":"Bensalem, S., et al.: Formal specification for learning-enabled autonomous systems (extended abstract). In: FoMLAS2022 (2022)","key":"1_CR4","DOI":"10.1007\/978-3-031-21222-2_8"},{"key":"1_CR5","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1016\/j.ress.2016.08.019","volume":"158","author":"P Bishop","year":"2017","unstructured":"Bishop, P., Povyakalo, A.: Deriving a frequentist conservative confidence bound for probability of failure per demand for systems with different operational and test profiles. Reliab. Eng. Syst. Saf. 158, 246\u2013253 (2017)","journal-title":"Reliab. Eng. Syst. Saf."},{"unstructured":"Demontis, A., et al.: Why do adversarial attacks transfer? Explaining transferability of evasion and poisoning attacks. In: 28th USENIX Security Symposium (USENIX Security 2019), Santa Clara, CA, August 2019, pp. 321\u2013338. USENIX Association (2019)","key":"1_CR6"},{"unstructured":"Du, S.S., Lee, J.D., Li, H., Wang, L., Zhai, X.: Gradient descent finds global minima of deep neural networks. arXiv e-prints, arXiv:1811.03804 (2018)","key":"1_CR7"},{"doi-asserted-by":"crossref","unstructured":"Dutle, A., et al.: From requirements to autonomous flight: an overview of the monitoring ICAROUS project. In: Proceedings of the 2nd Workshop on Formal Methods for Autonomous Systems. EPTCS, vol. 329, pp. 23\u201330 (2020)","key":"1_CR8","DOI":"10.4204\/EPTCS.329.3"},{"unstructured":"Fukunaga, K.: Introduction to Statistical Pattern Recognition. Elsevier (2013)","key":"1_CR9"},{"doi-asserted-by":"crossref","unstructured":"Gehr, T., Mirman, M., Drachsler-Cohen, D., Tsankov, P., Chaudhuri, S., Vechev, M.: AI2: safety and robustness certification of neural networks with abstract interpretation. In: 2018 IEEE Symposium on Security and Privacy (SP) (2018)","key":"1_CR10","DOI":"10.1109\/SP.2018.00058"},{"unstructured":"Huang, W., et al.: Coverage-guided testing for recurrent neural networks. IEEE Trans. Reliab. 1\u201316 (2021)","key":"1_CR11"},{"key":"1_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-63387-9_1","volume-title":"Computer Aided Verification","author":"X Huang","year":"2017","unstructured":"Huang, X., Kwiatkowska, M., Wang, S., Wu, M.: Safety verification of deep neural networks. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 3\u201329. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_1"},{"doi-asserted-by":"crossref","unstructured":"Jin, G., Yi, X., Huang, W., Schewe, S., Huang, X.: Enhancing adversarial training with second-order statistics of weights. In: CVPR 2022 (2022)","key":"1_CR13","DOI":"10.1109\/CVPR52688.2022.01484"},{"unstructured":"Jin, G., Yi, X., Zhang, L., Zhang, L., Schewe, S., Huang, X.: How does weight correlation affect the generalisation ability of deep neural networks. In: NeurIPS 2020 (2020)","key":"1_CR14"},{"issue":"3","key":"1_CR15","doi-asserted-by":"publisher","first-page":"521","DOI":"10.1007\/s10898-020-00952-6","volume":"79","author":"DR Jones","year":"2021","unstructured":"Jones, D.R., Martins, J.R.R.A.: The DIRECT algorithm: 25 years later. J. Glob. Optim. 79(3), 521\u2013566 (2021)","journal-title":"J. Glob. Optim."},{"key":"1_CR16","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/BF00941892","volume":"79","author":"DR Jones","year":"1993","unstructured":"Jones, D.R., Perttunen, C.D., Stuckman, B.E.: Lipschitzian optimization without the Lipschitz constant. J. Optim. Theory Appl. 79, 157\u2013181 (1993)","journal-title":"J. Optim. Theory Appl."},{"key":"1_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/978-3-319-63387-9_5","volume-title":"Computer Aided Verification","author":"G Katz","year":"2017","unstructured":"Katz, G., Barrett, C., Dill, D.L., Julian, K., Kochenderfer, M.J.: Reluplex: an efficient SMT solver for verifying deep neural networks. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 97\u2013117. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_5"},{"key":"1_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"296","DOI":"10.1007\/978-3-030-32304-2_15","volume-title":"Static Analysis","author":"J Li","year":"2019","unstructured":"Li, J., Liu, J., Yang, P., Chen, L., Huang, X., Zhang, L.: Analyzing deep neural networks with symbolic propagation: towards higher precision and faster verification. In: Chang, B.-Y.E. (ed.) SAS 2019. LNCS, vol. 11822, pp. 296\u2013319. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-32304-2_15"},{"issue":"5","key":"1_CR19","doi-asserted-by":"publisher","first-page":"1178","DOI":"10.1109\/TSE.2011.80","volume":"38","author":"B Littlewood","year":"2012","unstructured":"Littlewood, B., Rushby, J.: Reasoning about the reliability of diverse two-channel systems in which one channel is \u201cpossibly perfect\u2019\u2019. IEEE Transa. Softw. Eng. 38(5), 1178\u20131194 (2012)","journal-title":"IEEE Transa. Softw. Eng."},{"unstructured":"Madry, A., Makelov, A., Schmidt, L., Tsipras, D., Vladu, A.: Towards deep learning models resistant to adversarial attacks. In: ICLR 2018 (2018)","key":"1_CR20"},{"issue":"2","key":"1_CR21","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1109\/52.199724","volume":"10","author":"J Musa","year":"1993","unstructured":"Musa, J.: Operational profiles in software-reliability engineering. IEEE Softw. 10(2), 14\u201332 (1993)","journal-title":"IEEE Softw."},{"doi-asserted-by":"crossref","unstructured":"Orekondy, T., Schiele, B., Fritz, M.: Knockoff nets: stealing functionality of black-box models. In: IEEE Conference on Computer Vision and Pattern Recognition, CVPR 2019, Long Beach, CA, USA, 16\u201320 June 2019, pp. 4954\u20134963. Computer Vision Foundation\/IEEE (2019)","key":"1_CR22","DOI":"10.1109\/CVPR.2019.00509"},{"doi-asserted-by":"crossref","unstructured":"Pietrantuono, R., Popov, P., Russo, S.: Reliability assessment of service-based software under operational profile uncertainty. Reliab. Eng. Syst. Saf. 204, 107193 (2020)","key":"1_CR23","DOI":"10.1016\/j.ress.2020.107193"},{"doi-asserted-by":"crossref","unstructured":"Ruan, W., Huang, X., Kwiatkowska, M.: Reachability analysis of deep neural networks with provable guarantees. In: IJCAI, pp. 2651\u20132659 (2018)","key":"1_CR24","DOI":"10.24963\/ijcai.2018\/368"},{"doi-asserted-by":"crossref","unstructured":"Ruan, W., Wu, M., Sun, Y., Huang, X., Kroening, D., Kwiatkowska, M.: Global robustness evaluation of deep neural networks with provable guarantees for the hamming distance. In: IJCAI 2019, pp. 5944\u20135952 (2019)","key":"1_CR25","DOI":"10.24963\/ijcai.2019\/824"},{"doi-asserted-by":"crossref","unstructured":"Rushby, J.: Software verification and system assurance. In: 7th International Conference on Software Engineering and Formal Methods, Hanoi, Vietnam, pp. 3\u201310. IEEE (2009)","key":"1_CR26","DOI":"10.1109\/SEFM.2009.39"},{"unstructured":"Saddiki, H., Trapp, A.C., Flaherty, P.: A deterministic global optimization method for variational inference (2017)","key":"1_CR27"},{"doi-asserted-by":"crossref","unstructured":"Salako, K., Strigini, L., Zhao, X.: Conservative confidence bounds in safety, from generalised claims of improvement & statistical evidence. In: 51st Annual IEEE\/IFIP International Conference on Dependable Systems and Networks, DSN 2021, Taipei, Taiwan, pp. 451\u2013462. IEEE\/IFIP (2021)","key":"1_CR28","DOI":"10.1109\/DSN48987.2021.00055"},{"doi-asserted-by":"crossref","unstructured":"Sun, Y., Huang, X., Kroening, D.: Testing deep neural networks. CoRR, abs\/1803.04792 (2018)","key":"1_CR29","DOI":"10.1145\/3238147.3238172"},{"doi-asserted-by":"crossref","unstructured":"Sun, Y., Wu, M., Ruan, W., Huang, X., Kwiatkowska, M., Kroening, D.: Concolic testing for deep neural networks. In: 33rd IEEE\/ACM International Conference on Automated Software Engineering (ASE) (2018)","key":"1_CR30","DOI":"10.1145\/3238147.3238172"},{"doi-asserted-by":"crossref","unstructured":"Sun, Y., Wu, M., Ruan, W., Huang, X., Kwiatkowska, M., Kroening, D.: DeepConcolic: testing and debugging deep neural networks. In: 41st ACM\/IEEE International Conference on Software Engineering (ICSE 2019) (2019)","key":"1_CR31","DOI":"10.1109\/ICSE-Companion.2019.00051"},{"unstructured":"Szegedy, C., et al.: Intriguing properties of neural networks. In: ICLR. Citeseer (2014)","key":"1_CR32"},{"key":"1_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"408","DOI":"10.1007\/978-3-319-89960-2_22","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Wicker","year":"2018","unstructured":"Wicker, M., Huang, X., Kwiatkowska, M.: Feature-guided black-box safety testing of deep neural networks. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10805, pp. 408\u2013426. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89960-2_22"},{"issue":"01","key":"1_CR34","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1142\/S1469026809002461","volume":"08","author":"O Wirjadi","year":"2009","unstructured":"Wirjadi, O., Breuel, T.: A branch and bound algorithm for finding the modes in kernel density estimates. Int. J. Comput. Intell. Appl. 08(01), 17\u201335 (2009)","journal-title":"Int. J. Comput. Intell. Appl."},{"key":"1_CR35","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1016\/j.tcs.2019.05.046","volume":"807","author":"M Wu","year":"2020","unstructured":"Wu, M., Wicker, M., Ruan, W., Huang, X., Kwiatkowska, M.: A game-based approximate verification of deep neural networks with provable guarantees. Theor. Comput. Sci. 807, 298\u2013329 (2020)","journal-title":"Theor. Comput. Sci."},{"unstructured":"Xu, P., Ruan, W., Huang, X.: Towards the quantification of safety risks in deep neural networks. CoRR, abs\/2009.06114 (2020)","key":"1_CR36"},{"doi-asserted-by":"crossref","unstructured":"Xu, P., Ruan, W., Huang, X.: Quantifying safety risks of deep neural networks. Complex Intell. Syst. (2022)","key":"1_CR37","DOI":"10.1007\/s40747-022-00790-x"},{"doi-asserted-by":"crossref","unstructured":"Yang, Z., Zhang, J., Chang, E.-C., Liang, Z.: Neural network inversion in adversarial setting via background knowledge alignment. In: Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security, CCS 2019, pp. 225\u2013240. ACM, New York (2019)","key":"1_CR38","DOI":"10.1145\/3319535.3354261"},{"unstructured":"Zhao, X., et al.: Assessing reliability of deep learning through robustness evaluation and operational testing. In: AISafety2021 (2021)","key":"1_CR39"},{"unstructured":"Zhao, X., et al.: Reliability assessment and safety arguments for machine learning components in assuring learning-enabled autonomous systems. CoRR, abs\/2112.00646 (2021)","key":"1_CR40"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-17244-1_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,28]],"date-time":"2023-01-28T12:23:33Z","timestamp":1674908613000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-17244-1_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031172434","9783031172441"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-17244-1_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"10 October 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ICFEM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Formal Engineering Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Madrid","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Spain","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 October 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 October 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"icfem2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/maude.ucm.es\/ICFEM22\/index.html","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"61","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"23","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"38% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3 invited papers (two papers and one abstract)","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}