{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,23]],"date-time":"2026-08-23T11:21:05Z","timestamp":1787484065888,"version":"build-2736575974"},"reference-count":68,"publisher":"Association for Computing Machinery (ACM)","issue":"FSE","license":[{"start":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T00:00:00Z","timestamp":1750291200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"funder":[{"DOI":"10.13039\/501100012166","name":"National Key Research and Development Program of China","doi-asserted-by":"publisher","award":["2022YFB2702200"],"award-info":[{"award-number":["2022YFB2702200"]}],"id":[{"id":"10.13039\/501100012166","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["62172019"],"award-info":[{"award-number":["62172019"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001459","name":"Ministry of Education - Singapore","doi-asserted-by":"publisher","award":["MOE-T1-1\/2022-43"],"award-info":[{"award-number":["MOE-T1-1\/2022-43"]}],"id":[{"id":"10.13039\/501100001459","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001381","name":"National Research Foundation Singapore","doi-asserted-by":"publisher","award":["AISG2-GC-2023-008,NCRP25-P04-TAICeN"],"award-info":[{"award-number":["AISG2-GC-2023-008,NCRP25-P04-TAICeN"]}],"id":[{"id":"10.13039\/501100001381","id-type":"DOI","asserted-by":"publisher"}]}],"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-19T11:15:34Z","timestamp":1750331734000},"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":[{"vocabulary":"crossref","role":"author"}]},{"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":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7164-0580","authenticated-orcid":false,"given":"Zhe","family":"Hou","sequence":"additional","affiliation":[{"name":"Griffith University, Brisbane, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"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":[{"vocabulary":"crossref","role":"author"}]},{"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":[{"vocabulary":"crossref","role":"author"}]},{"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":[{"vocabulary":"crossref","role":"author"}]},{"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":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6550-7396","authenticated-orcid":false,"given":"Meng","family":"Sun","sequence":"additional","affiliation":[{"name":"Peking University, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,6,19]]},"reference":[{"key":"e_1_3_1_3_2","unstructured":"2023. Archive of Formal Proofs. https:\/\/www.isa-afp.org\/Accessd: 2024-01-19."},{"key":"e_1_3_1_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49665-7_19"},{"key":"e_1_3_1_5_2","doi-asserted-by":"crossref","unstructured":"Franz Baader and Tobias Nipkow. 1998. Term Rewriting and All That. Cambridge University Press.","DOI":"10.1017\/CBO9781139172752"},{"key":"e_1_3_1_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-013-9278-5"},{"key":"e_1_3_1_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-20615-8_1"},{"key":"e_1_3_1_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14203-1_9"},{"key":"e_1_3_1_9_2","doi-asserted-by":"publisher","unstructured":"Aline Brito Laerte Xavier Andre Hora and Marco Tulio Valente. 2018. APIDiff: Detecting API breaking changes. In 2018 IEEE 25th International Conference on Software Analysis Evolution and Reengineering (SANER). 507\u2013511. doi: 10.1109\/SANER.2018.8330249","DOI":"10.1109\/SANER.2018.8330249"},{"key":"e_1_3_1_10_2","unstructured":"The Coq Development Team. 2021. The Coq Proof Assistant Reference Manual -version 8.19.0. Technical Report. INRIA. https:\/\/hal.science\/hal-04523844"},{"key":"e_1_3_1_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21401-6_26"},{"key":"e_1_3_1_12_2","unstructured":"Manuel Eberl. 2015. Landau Symbols. Archive of Formal Proofs (July 2015).https:\/\/isa-afp.org\/entries\/Landau_Symbols.html Formal proof development."},{"key":"e_1_3_1_13_2","unstructured":"Chelsea Edmonds and Lawrence C. Paulson. 2021. Combinatorial Design Theory. Archive of Formal Proofs (August 2021). https:\/\/isa-afp.org\/entries\/Design_Theory.html Formal proof development."},{"key":"e_1_3_1_14_2","doi-asserted-by":"publisher","DOI":"10.1145\/3293882.3330571"},{"key":"e_1_3_1_15_2","unstructured":"Bertram Felgenhauer. 2015. Decreasing Diagrams II. Archive of Formal Proofs (August 2015). https:\/\/isa-afp.org\/entries\/Decreasing-Diagrams-II.html Formal proof development."},{"key":"e_1_3_1_16_2","doi-asserted-by":"publisher","DOI":"10.1145\/3611643.3616243"},{"key":"e_1_3_1_17_2","first-page":"305","volume-title":"An Introduction to Qualitative Research","author":"Flick Uwe","year":"2018","unstructured":"Uwe Flick. 2018. Coding and Categorizing. In An Introduction to Qualitative Research. SAGE Publications, Chapter 23, 305\u2013332."},{"key":"e_1_3_1_18_2","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 2019). https:\/\/isa-afp.org\/entries\/UTP.html Formal proof development."},{"key":"e_1_3_1_19_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2018.04.005"},{"key":"e_1_3_1_20_2","doi-asserted-by":"publisher","DOI":"10.1145\/3591221"},{"key":"e_1_3_1_21_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2022.18"},{"key":"e_1_3_1_22_2","first-page":"653","volume-title":"Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation","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 (Savannah, GA, USA) (OSDI\u201916). USENIX Association, USA, 653\u2013669."},{"key":"e_1_3_1_23_2","doi-asserted-by":"publisher","unstructured":"Hao Guan Ying Xiao Jiaying Li Yepang Liu and Guangdong Bai. 2023. A Comprehensive Study of Real-World Bugs in Machine Learning Model Optimization. In 2023 IEEE\/ACM 45th International Conference on Software Engineering (ICSE). 147\u2013158. doi: 10.1109\/ICSE48619.2023.00024","DOI":"10.1109\/ICSE48619.2023.00024"},{"key":"e_1_3_1_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/3460319.3464796"},{"key":"e_1_3_1_25_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10664-021-10096-0"},{"key":"e_1_3_1_26_2","doi-asserted-by":"publisher","unstructured":"Huaxun Huang Ming Wen Lili Wei Yepang Liu and Shing-Chi Cheung. 2021. Characterizing and Detecting Configuration Compatibility Issues in Android Apps. In 2021 36th IEEE\/ACM International Conference on Automated Software Engineering (ASE). 517\u2013528. doi: 10.1109\/ASE51524.2021.9678556","DOI":"10.1109\/ASE51524.2021.9678556"},{"key":"e_1_3_1_27_2","doi-asserted-by":"publisher","DOI":"10.1145\/3597926.3598074"},{"key":"e_1_3_1_28_2","first-page":"8360","article-title":"Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers","volume":"35","author":"Qiaochu Jiang Albert","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.), Vol. 35. Curran Associates, Inc., 8360\u20138373. https:\/\/proceedings.neurips.cc\/paper_files\/paper\/2022\/file\/377c25312668e48f2e531e2f2c422483-Paper-Conference.pdf","journal-title":"Advances in Neural Information Processing Systems"},{"key":"e_1_3_1_29_2","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_3_1_30_2","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_3_1_31_2","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535841"},{"key":"e_1_3_1_32_2","unstructured":"Peter Lammich. 2009. Collections Framework. Archive of Formal Proofs (November 2009). https:\/\/isa-afp.org\/entries\/Collections.html Formal proof development."},{"key":"e_1_3_1_33_2","unstructured":"Peter Lammich and Rene Meis. 2012. A Separation Logic Framework for Imperative HOL. Archive of Formal Proofs (November 2012). https:\/\/isa-afp.org\/entries\/Separation_Logic_Imperative_HOL.html Formal proof development."},{"key":"e_1_3_1_34_2","volume-title":"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. SEE, Toulouse, France. https:\/\/inria.hal.science\/hal-01238879"},{"key":"e_1_3_1_35_2","doi-asserted-by":"publisher","DOI":"10.1145\/3213846.3213857"},{"key":"e_1_3_1_36_2","doi-asserted-by":"publisher","DOI":"10.1145\/3196398.3196419"},{"key":"e_1_3_1_37_2","doi-asserted-by":"publisher","DOI":"10.1145\/3533767.3534407"},{"key":"e_1_3_1_38_2","doi-asserted-by":"publisher","DOI":"10.1145\/3624737"},{"key":"e_1_3_1_39_2","unstructured":"Andreas Lochbihler. 2013. Native Word. Archive of Formal Proofs (September 2013). https:\/\/isa-afp.org\/entries\/Native_Word.html Formal proof development."},{"key":"e_1_3_1_40_2","unstructured":"Alexander Lochmann and Bertram Felgenhauer. 2022. First-Order Theory of Rewriting. Archive of Formal Proofs (February 2022). https:\/\/isa-afp.org\/entries\/FO_Theory_Rewriting.html Formal proof development."},{"key":"e_1_3_1_41_2","doi-asserted-by":"publisher","unstructured":"Xiaokun Luan David Miguel Sanan Baena Zhe Hou Qiyuan Xu Chengwei Liu Yufan Cai Yang Liu and Meng Sun. 2025. Reproduction Package and Data for Article \u2018Why the Proof Fails in Different Versions of Theorem Provers: An Empirical Study of Compatibility Issues in Isabelle\u2019. (Feb. 2025). doi: 10.6084\/m9.figshare.25912954.v1","DOI":"10.6084\/m9.figshare.25912954.v1"},{"key":"e_1_3_1_42_2","doi-asserted-by":"publisher","unstructured":"Tarek Mahmud Meiru Che and Guowei Yang. 2021. Android Compatibility Issue Detection Using API Differences. In 2021 IEEE International Conference on Software Analysis Evolution and Reengineering (SANER). 480\u2013490. doi: 10.1109\/SANER50967.2021.00051","DOI":"10.1109\/SANER50967.2021.00051"},{"key":"e_1_3_1_43_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2023.3274153"},{"key":"e_1_3_1_44_2","doi-asserted-by":"publisher","DOI":"10.1145\/3372885.3373824"},{"key":"e_1_3_1_45_2","doi-asserted-by":"publisher","unstructured":"Tobias Nipkow Markus Wenzel and Lawrence C Paulson. 2002. Isabelle\/HOL: a proof assistant for higher-order logic. Springer. doi: 10.1007\/3-540-45949-9","DOI":"10.1007\/3-540-45949-9"},{"key":"e_1_3_1_46_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10664-021-10052-y"},{"key":"e_1_3_1_47_2","doi-asserted-by":"publisher","unstructured":"Lawrence C. Paulson. 1998. A generic tableau prover and its integration with Isabelle. Technical Report UCAM-CL-TR-441. University of Cambridge Computer Laboratory. doi: 10.48456\/tr-441","DOI":"10.48456\/tr-441"},{"key":"e_1_3_1_48_2","unstructured":"Lawrence C. Paulson. 2019. Zermelo Fraenkel Set Theory in Higher-Order Logic. Archive of Formal Proofs (October 2019). https:\/\/isa-afp.org\/entries\/ZFC_in_HOL.html Formal proof development."},{"key":"e_1_3_1_49_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74591-4_18"},{"key":"e_1_3_1_50_2","unstructured":"Stanislas Polu and Ilya Sutskever. 2020. Generative Language Modeling for Automated Theorem Proving. arXiv:2009.03393 [cs.LG] https:\/\/arxiv.org\/abs\/2009.03393"},{"key":"e_1_3_1_51_2","doi-asserted-by":"crossref","unstructured":"Andrei Popescu and Johannes H\u00f6lzl. 2014. Probabilistic Noninterference. Archive of Formal Proofs (March 2014). https:\/\/isa-afp.org\/entries\/Probabilistic_Noninterference.html Formal proof development.","DOI":"10.1007\/978-3-319-03545-1_17"},{"key":"e_1_3_1_52_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2023.26"},{"key":"e_1_3_1_53_2","doi-asserted-by":"publisher","DOI":"10.1561\/2500000045"},{"key":"e_1_3_1_54_2","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454033"},{"key":"e_1_3_1_55_2","doi-asserted-by":"publisher","DOI":"10.1145\/3167094"},{"key":"e_1_3_1_56_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2019.26"},{"key":"e_1_3_1_57_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10664-008-9102-8"},{"key":"e_1_3_1_58_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_6"},{"key":"e_1_3_1_59_2","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. doi: 10.1109\/ICSE-Companion52605.2021.00022","DOI":"10.1109\/ICSE-Companion52605.2021.00022"},{"key":"e_1_3_1_60_2","doi-asserted-by":"publisher","DOI":"10.1145\/3551349.3560437"},{"key":"e_1_3_1_61_2","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_3_1_62_2","doi-asserted-by":"publisher","DOI":"10.1145\/3611643.3616321"},{"key":"e_1_3_1_63_2","unstructured":"Makarius Wenzel. 2024. The Isabelle\/Isar Reference Manual. https:\/\/isabelle.in.tum.de\/dist\/Isabelle2024\/doc\/isar-ref.pdf"},{"key":"e_1_3_1_64_2","doi-asserted-by":"publisher","DOI":"10.1145\/2854065.2854081"},{"key":"e_1_3_1_65_2","doi-asserted-by":"publisher","unstructured":"Laerte Xavier Aline Brito Andre Hora and Marco Tulio Valente. 2017. Historical and impact analysis of API breaking changes: A large-scale study. In 2017 IEEE 24th International Conference on Software Analysis Evolution and Reengineering (SANER). 138\u2013147. doi: 10.1109\/SANER.2017.7884616","DOI":"10.1109\/SANER.2017.7884616"},{"key":"e_1_3_1_66_2","doi-asserted-by":"publisher","DOI":"10.1145\/3518994"},{"key":"e_1_3_1_67_2","doi-asserted-by":"publisher","unstructured":"Weiwei Xu Hao He Kai Gao and Minghui Zhou. 2023. Understanding and Remediating Open-Source License Incompatibilities in the PyPI Ecosystem. In 2023 38th IEEE\/ACM International Conference on Automated Software Engineering (ASE). 178\u2013190. doi: 10.1109\/ASE56229.2023.00175","DOI":"10.1109\/ASE56229.2023.00175"},{"key":"e_1_3_1_68_2","doi-asserted-by":"publisher","unstructured":"Sen Yang Sen Chen Lingling Fan Sihan Xu Zhanwei Hui and Song Huang. 2023. Compatibility Issue Detection for Android Apps Based on Path-Sensitive Semantic Analysis. In 2023 IEEE\/ACM 45th International Conference on Software Engineering (ICSE). 257\u2013269. doi: 10.1109\/ICSE48619.2023.00033","DOI":"10.1109\/ICSE48619.2023.00033"},{"key":"e_1_3_1_69_2","doi-asserted-by":"publisher","DOI":"10.1145\/3551349.3556956"},{"key":"e_1_3_1_70_2","doi-asserted-by":"publisher","unstructured":"Zhaoxu Zhang Hengcheng Zhu Ming Wen Yida Tao Yepang Liu and Yingfei Xiong. 2020. How Do Python Framework APIs Evolve? An Exploratory Study. In 2020 IEEE 27th International Conference on Software Analysis Evolution and Reengineering (SANER). 81\u201392. doi: 10.1109\/SANER48275.2020.9054800","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":[[2026,8,23]],"date-time":"2026-08-23T10:58:21Z","timestamp":1787482701000},"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]]}}}