{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,18]],"date-time":"2026-04-18T23:00:17Z","timestamp":1776553217177,"version":"3.51.2"},"reference-count":68,"publisher":"Association for Computing Machinery (ACM)","issue":"FSE","funder":[{"name":"National Key Research and Development Program of China","award":["2022YFB2702200"],"award-info":[{"award-number":["2022YFB2702200"]}]},{"name":"National Natural Science Foundation of China","award":["62172019"],"award-info":[{"award-number":["62172019"]}]},{"name":"Ministry of Education - Singapore","award":["MOE-T1-1\\\/2022-43"],"award-info":[{"award-number":["MOE-T1-1\\\/2022-43"]}]},{"name":"National Research Foundation Singapore","award":["AISG2-GC-2023-008,NCRP25-P04-TAICeN"],"award-info":[{"award-number":["AISG2-GC-2023-008,NCRP25-P04-TAICeN"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Proc. ACM Softw. Eng."],"published-print":{"date-parts":[[2025,6,19]]},"abstract":"<jats:p>Proof assistants are software tools for formal modeling and verification of software, hardware, design, and mathematical proofs. Due to the growing complexity and scale of formal proofs, compatibility issues frequently arise when using different versions of proof assistants. These issues result in broken proofs, disrupting the maintenance of formalized theories and hindering the broader dissemination of results within the community. Although existing works have proposed techniques to address specific types of compatibility issues, the overall characteristics of these issues remain largely unexplored. To address this gap, we conduct the first extensive empirical study to characterize compatibility issues, using Isabelle as a case study. We develop a regression testing framework to automatically collect compatibility issues from the Archive of Formal Proofs, the largest repository of formal proofs in Isabelle. By analyzing 12,079 collected issues, we identify their types and symptoms and further investigate their root causes. We also extract updated proofs that address these issues to understand the applied resolution strategies. Our study provides an in-depth understanding of compatibility issues in proof assistants, offering insights that support the development of effective techniques to mitigate these issues.<\/jats:p>","DOI":"10.1145\/3715787","type":"journal-article","created":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T15:15:34Z","timestamp":1750346134000},"page":"1499-1521","source":"Crossref","is-referenced-by-count":1,"title":["Why the Proof Fails in Different Versions of Theorem Provers: An Empirical Study of Compatibility Issues in Isabelle"],"prefix":"10.1145","volume":"2","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5878-6486","authenticated-orcid":false,"given":"Xiaokun","family":"Luan","sequence":"first","affiliation":[{"name":"Peking University, Beijing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2755-3089","authenticated-orcid":false,"given":"David","family":"Sanan","sequence":"additional","affiliation":[{"name":"Singapore Institute of Technology, Singapore, Singapore"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7164-0580","authenticated-orcid":false,"given":"Zhe","family":"Hou","sequence":"additional","affiliation":[{"name":"Griffith University, Brisbane, Australia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9196-3237","authenticated-orcid":false,"given":"Qiyuan","family":"Xu","sequence":"additional","affiliation":[{"name":"Nanyang Technological University, Singapore, Singapore"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1175-2753","authenticated-orcid":false,"given":"Chengwei","family":"Liu","sequence":"additional","affiliation":[{"name":"Nanyang Technological University, Singapore, Singapore"},{"name":"China-Singapore International Joint Research Institute, Guangzhou, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-7579-0824","authenticated-orcid":false,"given":"Yufan","family":"Cai","sequence":"additional","affiliation":[{"name":"National University of Singapore, Singapore, Singapore"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7300-9215","authenticated-orcid":false,"given":"Yang","family":"Liu","sequence":"additional","affiliation":[{"name":"Nanyang Technological University, Singapore, Singapore"},{"name":"China-Singapore International Joint Research Institute, Guangzhou, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6550-7396","authenticated-orcid":false,"given":"Meng","family":"Sun","sequence":"additional","affiliation":[{"name":"Peking University, Beijing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,6,19]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"2023. Archive of Formal Proofs. https:\/\/www.isa-afp.org\/ Accessd: 2024-01-19"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49665-7_19"},{"key":"e_1_2_1_3_1","volume-title":"Term Rewriting and All That","author":"Baader Franz","unstructured":"Franz Baader and Tobias Nipkow. 1998. Term Rewriting and All That. Cambridge University Press."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-013-9278-5"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-20615-8_1"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14203-1_9"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/SANER.2018.8330249"},{"key":"e_1_2_1_8_1","unstructured":"The Coq Development Team. 2021. The Coq Proof Assistant Reference Manual - version 8.19.0. INRIA. https:\/\/hal.science\/hal-04523844"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21401-6_26"},{"key":"e_1_2_1_10_1","unstructured":"Manuel Eberl. 2015. Landau Symbols. Archive of Formal Proofs July issn:2150-914x https:\/\/isa-afp.org\/entries\/Landau_Symbols.html"},{"key":"e_1_2_1_11_1","volume-title":"Paulson","author":"Edmonds Chelsea","year":"2021","unstructured":"Chelsea Edmonds and Lawrence C. Paulson. 2021. Combinatorial Design Theory. Archive of Formal Proofs, August, issn:2150-914x https:\/\/isa-afp.org\/entries\/Design_Theory.html"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293882.3330571"},{"key":"e_1_2_1_13_1","unstructured":"Bertram Felgenhauer. 2015. Decreasing Diagrams II. Archive of Formal Proofs August issn:2150-914x https:\/\/isa-afp.org\/entries\/Decreasing-Diagrams-II.html"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3611643.3616243"},{"key":"e_1_2_1_15_1","volume-title":"An Introduction to Qualitative Research","author":"Flick Uwe","unstructured":"Uwe Flick. 2018. Coding and Categorizing. In An Introduction to Qualitative Research. SAGE Publications, 305\u2013332. isbn:9781526464224"},{"key":"e_1_2_1_16_1","unstructured":"Simon Foster Frank Zeyda Yakoub Nemouchi Pedro Ribeiro and Burkhart Wolff. 2019. Isabelle\/UTP: Mechanised Theory Engineering for Unifying Theories of Programming. Archive of Formal Proofs February issn:2150-914x https:\/\/isa-afp.org\/entries\/UTP.html"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2018.04.005"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591221"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2022.18"},{"key":"e_1_2_1_20_1","volume-title":"Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation (OSDI\u201916)","author":"Gu Ronghui","year":"2016","unstructured":"Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan Wu, Jieung Kim, Vilhelm Sj\u00f6berg, and David Costanzo. 2016. CertiKOS: an extensible architecture for building certified concurrent OS kernels. In Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation (OSDI\u201916). USENIX Association, USA. 653\u2013669. isbn:9781931971331"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE48619.2023.00024"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3460319.3464796"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10664-021-10096-0"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE51524.2021.9678556"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3597926.3598074"},{"key":"e_1_2_1_26_1","volume-title":"Yuhuai Wu, and Mateja Jamnik.","author":"Jiang Albert Qiaochu","year":"2022","unstructured":"Albert Qiaochu Jiang, Wenda Li, Szymon Tworkowski, Konrad Czechowski, Tomasz Odrzyg\u00f3\u017ad\u017a, Piotr Mi\u0142 o\u015b, Yuhuai Wu, and Mateja Jamnik. 2022. Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers. In Advances in Neural Information Processing Systems, S. Koyejo, S. Mohamed, A. Agarwal, D. Belgrave, K. Cho, and A. Oh (Eds.). 35, Curran Associates, Inc., 8360\u20138373. https:\/\/proceedings.neurips.cc\/paper_files\/paper\/2022\/file\/377c25312668e48f2e531e2f2c422483-Paper-Conference.pdf"},{"key":"e_1_2_1_27_1","volume-title":"The Eleventh International Conference on Learning Representations. https:\/\/openreview.net\/forum?id=SMa9EAovKMC","author":"Jiang Albert Qiaochu","year":"2023","unstructured":"Albert Qiaochu Jiang, Sean Welleck, Jin Peng Zhou, Timothee Lacroix, Jiacheng Liu, Wenda Li, Mateja Jamnik, Guillaume Lample, and Yuhuai Wu. 2023. Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs. In The Eleventh International Conference on Learning Representations. https:\/\/openreview.net\/forum?id=SMa9EAovKMC"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535841"},{"key":"e_1_2_1_30_1","unstructured":"Peter Lammich. 2009. Collections Framework. Archive of Formal Proofs November issn:2150-914x https:\/\/isa-afp.org\/entries\/Collections.html"},{"key":"e_1_2_1_31_1","unstructured":"Peter Lammich and Rene Meis. 2012. A Separation Logic Framework for Imperative HOL. Archive of Formal Proofs November issn:2150-914x https:\/\/isa-afp.org\/entries\/Separation_Logic_Imperative_HOL.html"},{"key":"e_1_2_1_32_1","volume-title":"CompCert - A Formally Verified Optimizing Compiler. In ERTS 2016: Embedded Real Time Software and Systems, 8th European Congress","author":"Leroy Xavier","year":"2016","unstructured":"Xavier Leroy, Sandrine Blazy, Daniel K\u00e4stner, Bernhard Schommer, Markus Pister, and Christian Ferdinand. 2016. CompCert - A Formally Verified Optimizing Compiler. In ERTS 2016: Embedded Real Time Software and Systems, 8th European Congress. Toulouse, France. https:\/\/inria.hal.science\/hal-01238879"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3213846.3213857"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3196398.3196419"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3533767.3534407"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3624737"},{"key":"e_1_2_1_37_1","unstructured":"Andreas Lochbihler. 2013. Native Word. Archive of Formal Proofs September issn:2150-914x https:\/\/isa-afp.org\/entries\/Native_Word.html"},{"key":"e_1_2_1_38_1","unstructured":"Alexander Lochmann and Bertram Felgenhauer. 2022. First-Order Theory of Rewriting. Archive of Formal Proofs February issn:2150-914x https:\/\/isa-afp.org\/entries\/FO_Theory_Rewriting.html"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.6084\/m9.figshare.25912954.v1"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/SANER50967.2021.00051"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2023.3274153"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3372885.3373824"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10664-021-10052-y"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.48456\/tr-441"},{"key":"e_1_2_1_46_1","unstructured":"Lawrence C. Paulson. 2019. Zermelo Fraenkel Set Theory in Higher-Order Logic. Archive of Formal Proofs October issn:2150-914x https:\/\/isa-afp.org\/entries\/ZFC_in_HOL.html"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74591-4_18"},{"key":"e_1_2_1_48_1","unstructured":"Stanislas Polu and Ilya Sutskever. 2020. Generative Language Modeling for Automated Theorem Proving. arxiv:2009.03393. arxiv:2009.03393"},{"key":"e_1_2_1_49_1","unstructured":"Andrei Popescu and Johannes H\u00f6lzl. 2014. Probabilistic Noninterference. Archive of Formal Proofs March issn:2150-914x https:\/\/isa-afp.org\/entries\/Probabilistic_Noninterference.html"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2023.26"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1561\/2500000045"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454033"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3167094"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2019.26"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10664-008-9102-8"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_6"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","unstructured":"Aparna Vadlamani Rishitha Kalicheti and Sridhar Chimalakonda. 2021. APIScanner - Towards Automated Detection of Deprecated APIs in Python Libraries. In 2021 IEEE\/ACM 43rd International Conference on Software Engineering: Companion Proceedings (ICSE-Companion). 5\u20138. https:\/\/doi.org\/10.1109\/ICSE-Companion52605.2021.00022 10.1109\/ICSE-Companion52605.2021.00022","DOI":"10.1109\/ICSE-Companion52605.2021.00022"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/3551349.3560437"},{"key":"e_1_2_1_59_1","volume-title":"LEGO-Prover: Neural Theorem Proving with Growing Libraries. In The Twelfth International Conference on Learning Representations. https:\/\/openreview.net\/forum?id=3f5PALef5B","author":"Wang Haiming","year":"2024","unstructured":"Haiming Wang, Huajian Xin, Chuanyang Zheng, Zhengying Liu, Qingxing Cao, Yinya Huang, Jing Xiong, Han Shi, Enze Xie, Jian Yin, Zhenguo Li, and Xiaodan Liang. 2024. LEGO-Prover: Neural Theorem Proving with Growing Libraries. In The Twelfth International Conference on Learning Representations. https:\/\/openreview.net\/forum?id=3f5PALef5B"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/3611643.3616321"},{"key":"e_1_2_1_61_1","unstructured":"Makarius Wenzel. 2024. The Isabelle\/Isar Reference Manual. https:\/\/isabelle.in.tum.de\/dist\/Isabelle2024\/doc\/isar-ref.pdf"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/2854065.2854081"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1109\/SANER.2017.7884616"},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/3518994"},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE56229.2023.00175"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE48619.2023.00033"},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/3551349.3556956"},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1109\/SANER48275.2020.9054800"}],"container-title":["Proceedings of the ACM on Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3715787","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T15:20:56Z","timestamp":1750346456000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3715787"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,19]]},"references-count":68,"journal-issue":{"issue":"FSE","published-print":{"date-parts":[[2025,6,19]]}},"alternative-id":["10.1145\/3715787"],"URL":"https:\/\/doi.org\/10.1145\/3715787","relation":{},"ISSN":["2994-970X"],"issn-type":[{"value":"2994-970X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,6,19]]}}}