{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,31]],"date-time":"2026-03-31T14:28:50Z","timestamp":1774967330529,"version":"3.50.1"},"reference-count":98,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0\/"}],"funder":[{"DOI":"10.13039\/100009392","name":"Prince Sattam Bin Abdulaziz University","doi-asserted-by":"publisher","award":["PSAU\/2023\/R\/1444"],"award-info":[{"award-number":["PSAU\/2023\/R\/1444"]}],"id":[{"id":"10.13039\/100009392","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Access"],"published-print":{"date-parts":[[2024]]},"DOI":"10.1109\/access.2024.3420415","type":"journal-article","created":{"date-parts":[[2024,6,28]],"date-time":"2024-06-28T18:42:33Z","timestamp":1719600153000},"page":"90299-90316","source":"Crossref","is-referenced-by-count":34,"title":["Guaranteeing Correctness in Black-Box Machine Learning: A Fusion of Explainable AI and Formal Methods for Healthcare Decision-Making"],"prefix":"10.1109","volume":"12","author":[{"ORCID":"https:\/\/orcid.org\/0009-0008-5713-5578","authenticated-orcid":false,"given":"Nadia","family":"Khan","sequence":"first","affiliation":[{"name":"Department of Software Engineering, Faculty of Computing, The Islamia University of Bahawalpur, Punjab, Pakistan"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3173-2549","authenticated-orcid":false,"given":"Muhammad","family":"Nauman","sequence":"additional","affiliation":[{"name":"Department of Software Engineering, Faculty of Computing, The Islamia University of Bahawalpur, Punjab, Pakistan"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8665-1669","authenticated-orcid":false,"given":"Ahmad S.","family":"Almadhor","sequence":"additional","affiliation":[{"name":"College of Computer and Information Sciences, Jouf University, Sakaka, Saudi Arabia"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2475-5590","authenticated-orcid":false,"given":"Nadeem","family":"Akhtar","sequence":"additional","affiliation":[{"name":"Department of Software Engineering, Faculty of Computing, The Islamia University of Bahawalpur, Punjab, Pakistan"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2074-0658","authenticated-orcid":false,"given":"Abdullah","family":"Alghuried","sequence":"additional","affiliation":[{"name":"Department of Industrial Engineering, Faculty of Engineering, University of Tabuk, Tabuk, Saudi Arabia"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7201-6963","authenticated-orcid":false,"given":"Adi","family":"Alhudhaif","sequence":"additional","affiliation":[{"name":"Department of Computer Science, College of Computer Engineering and Sciences in Al-Kharj, Prince Sattam Bin Abdulaziz University, Al-Kharj, Saudi Arabia"}]}],"member":"263","reference":[{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.3390\/e23010018"},{"issue":"2","key":"ref2","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1016\/j.cjca.2021.10.009","article-title":"AI in cardiovascular imaging: \u2018Unexplainable\u2019 legal and ethical challenges?","volume":"38","author":"Lang","year":"2021","journal-title":"Can. J. Cardiol."},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2021.103471"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1016\/j.inffus.2019.12.012"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-65965-3_28"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1145\/3301275.3308446"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1145\/3297280.3297328"},{"key":"ref8","article-title":"A human-grounded evaluation of SHAP for alert processing","author":"Weerts","year":"2019","journal-title":"arXiv:1907.03324"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.3390\/cancers13143450"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.24018\/ejfood.2022.4.6.348"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1109\/BIBM52615.2021.9669648"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1016\/j.powtec.2023.118416"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45697-9_2"},{"key":"ref14","doi-asserted-by":"crossref","first-page":"42","DOI":"10.1016\/j.artmed.2019.01.001","article-title":"Explainable artificial intelligence for breast cancer: A visual case-based reasoning approach","volume":"94","author":"Lamy","year":"2019","journal-title":"Artif. Intell. Med."},{"issue":"9","key":"ref15","doi-asserted-by":"crossref","first-page":"2443","DOI":"10.3390\/cancers15092443","article-title":"A hybrid algorithm of ML and XAI to prevent breast cancer: A strategy to support decision making","volume":"15","author":"Silva-Aravena","year":"2023","journal-title":"Cancers"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-31414-8_2"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.3390\/diagnostics12020237"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1109\/TRPMS.2021.3066428"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1109\/BigData50022.2020.9378081"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1109\/DSAA.2018.00018"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2021.3121092"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-30823-9_10"},{"key":"ref23","article-title":"Recent advances in formal explainability","author":"Huang","year":"2023"},{"key":"ref24","article-title":"The theory and practice of a formal method: NewCoRe","volume-title":"Proc. IFIP World Comput. Congr.","author":"Holzmann"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-70848-5_6"},{"key":"ref26","first-page":"20","article-title":"Verification and validation of autonomy software at NASA","author":"Pecheur","year":"2000"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.3390\/make3010010"},{"key":"ref28","first-page":"895","article-title":"Model-agnostic counterfactual explanations for consequential decisions","volume-title":"Proc. 23rd Int. Conf. Artif. Intell. Statist. (AISTATS)","volume":"108","author":"Karimi"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1109\/ICPHYS.2018.8387644"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-47919-2_10"},{"key":"ref31","article-title":"Kommunikation mit automaten","author":"Petri","year":"1962"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44919-1_28"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02424-5_19"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1109\/TNNLS.2016.2599820"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1109\/TPAMI.2018.2858759"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1109\/ICCV.2017.74"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2023.3269694"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-50402-1_4"},{"key":"ref39","first-page":"1472","article-title":"A prediction and recommendation system for diabetes mellitus using XAI-based lime explainer","volume-title":"Proc. Int. Conf. Sustain. Comput. Data Commun. Syst. (ICSCDS)","author":"Nagaraj"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1016\/j.media.2022.102470"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.1023\/A:1009738307837"},{"key":"ref42","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v32i1.11491"},{"key":"ref43","article-title":"Local interpretable model-agnostic explanations of Bayesian predictive models via Kullback\u2013Leibler projections","author":"Peltola","year":"2018","journal-title":"arXiv:1810.02678"},{"key":"ref44","article-title":"NormLime: A new feature importance metric for explaining deep neural networks","author":"Ahern","year":"2019","journal-title":"arXiv:1909.04200"},{"key":"ref45","doi-asserted-by":"crossref","DOI":"10.1016\/j.knosys.2024.111732","article-title":"BMB-LIME: LIME with modeling local nonlinearity and uncertainty in explainability","volume":"294","author":"Hung","year":"2024","journal-title":"Knowl.-Based Syst."},{"key":"ref46","doi-asserted-by":"publisher","DOI":"10.5860\/choice.194685"},{"key":"ref47","volume-title":"Industrial Use of Safety-Related Artificial Neural Networks","author":"Lisboa","year":"2001"},{"key":"ref48","doi-asserted-by":"publisher","DOI":"10.1016\/j.heliyon.2018.e00938"},{"key":"ref49","doi-asserted-by":"publisher","DOI":"10.1016\/j.solener.2019.01.037"},{"key":"ref50","doi-asserted-by":"publisher","DOI":"10.1080\/014311697218700"},{"key":"ref51","doi-asserted-by":"publisher","DOI":"10.1145\/1190095.1190171"},{"key":"ref52","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/2319.001.0001"},{"key":"ref53","doi-asserted-by":"publisher","DOI":"10.1109\/5.24143"},{"key":"ref54","doi-asserted-by":"publisher","DOI":"10.1007\/bfb0025774"},{"key":"ref55","volume-title":"Principles of Model Checking","author":"Baier","year":"2008"},{"key":"ref56","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2019.2949286"},{"key":"ref57","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2021.3105956"},{"key":"ref58","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2023.3308446"},{"key":"ref59","doi-asserted-by":"publisher","DOI":"10.1016\/j.eswa.2016.11.017"},{"key":"ref60","doi-asserted-by":"publisher","DOI":"10.1109\/TNN.2005.863472"},{"key":"ref61","doi-asserted-by":"publisher","DOI":"10.1109\/69.824621"},{"key":"ref62","doi-asserted-by":"publisher","DOI":"10.1109\/2.485895"},{"key":"ref63","doi-asserted-by":"publisher","DOI":"10.1162\/neco.1997.9.1.205"},{"key":"ref64","doi-asserted-by":"publisher","DOI":"10.1007\/978-981-10-4642-1_5"},{"key":"ref65","doi-asserted-by":"publisher","DOI":"10.1016\/j.bspc.2021.103141"},{"key":"ref66","doi-asserted-by":"publisher","DOI":"10.1016\/j.measurement.2019.05.022"},{"key":"ref67","doi-asserted-by":"publisher","DOI":"10.1016\/j.asoc.2019.105941"},{"key":"ref68","doi-asserted-by":"publisher","DOI":"10.1007\/s12650-019-00607-z"},{"key":"ref69","doi-asserted-by":"publisher","DOI":"10.1145\/3313831.3376590"},{"key":"ref70","doi-asserted-by":"publisher","DOI":"10.1145\/3351095.3375624"},{"key":"ref71","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2020.2976199"},{"key":"ref72","doi-asserted-by":"publisher","DOI":"10.1109\/ICMLA.2019.00308"},{"key":"ref73","doi-asserted-by":"publisher","DOI":"10.1109\/ICSSIT46314.2019.8987766"},{"key":"ref74","doi-asserted-by":"publisher","DOI":"10.1109\/DASC\/PiCom\/DataCom\/CyberSciTec.2018.00052"},{"key":"ref75","doi-asserted-by":"publisher","DOI":"10.1007\/s11063-011-9207-8"},{"key":"ref76","doi-asserted-by":"publisher","DOI":"10.1109\/IJCNN.2001.938448"},{"key":"ref77","doi-asserted-by":"publisher","DOI":"10.1109\/72.809084"},{"key":"ref78","doi-asserted-by":"publisher","DOI":"10.1016\/S0957-4174(99)80008-6"},{"issue":"1","key":"ref79","first-page":"33","article-title":"A novel interpretable web-based tool on the associative classification methods: An application on breast cancer dataset","volume":"5","author":"Arslan","year":"2020","journal-title":"J. Cogn. Syst."},{"key":"ref80","doi-asserted-by":"publisher","DOI":"10.1109\/ICECCS59891.2023.00012"},{"key":"ref81","article-title":"Formal methods meet XAI: The tool DEGARI 2.0 for social inclusion","volume-title":"Proc. 4th Workshop Artif. Intell. Formal Verification, Logic, Automata, Synthesis","author":"Antonio"},{"key":"ref82","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-46002-9_7"},{"key":"ref83","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-19759-8_24"},{"key":"ref84","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v36i11.21499"},{"key":"ref85","doi-asserted-by":"publisher","DOI":"10.34727\/2023\/isbn.978-3-85448-060-0_9"},{"key":"ref86","doi-asserted-by":"publisher","DOI":"10.1016\/j.ijar.2023.109112"},{"key":"ref87","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2023.3298569"},{"key":"ref88","doi-asserted-by":"crossref","DOI":"10.1016\/j.eswa.2023.120130","article-title":"XAI-MethylMarker: Explainable AI approach for biomarker discovery for breast cancer subtype classification using methylation data","volume":"225","author":"Rajpal","year":"2023","journal-title":"Expert Syst. Appl."},{"key":"ref89","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-07704-3_26"},{"key":"ref90","volume-title":"UCI Machine Learning Repository","author":"Dua","year":"2022"},{"key":"ref91","doi-asserted-by":"publisher","DOI":"10.1007\/s10115-011-0463-8"},{"key":"ref92","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2021.3088901"},{"key":"ref93","volume-title":"C4. 5: Programs for Machine Learning","author":"Quinlan","year":"2014"},{"key":"ref94","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-09823-4_66"},{"key":"ref95","volume-title":"Cpntools Home","author":"Jensen","year":"2022"},{"key":"ref96","doi-asserted-by":"publisher","DOI":"10.1016\/j.mlwa.2023.100492"},{"key":"ref97","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-68640-6"},{"key":"ref98","article-title":"A unified approach to interpreting model predictions","volume-title":"Proc. Adv. Neural Inf. Process. Syst.","volume":"30","author":"Lundberg"}],"container-title":["IEEE Access"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx8\/6287639\/10380310\/10577273.pdf?arnumber=10577273","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,7]],"date-time":"2024-07-07T05:34:41Z","timestamp":1720330481000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/10577273\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"references-count":98,"URL":"https:\/\/doi.org\/10.1109\/access.2024.3420415","relation":{},"ISSN":["2169-3536"],"issn-type":[{"value":"2169-3536","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024]]}}}