Reproduction Package and Data for Article 'Why the Proof Fails in Different Versions of Theorem Provers: An Empirical Study of Compatibility Issues in Isabelle'

<p><br></p><p dir="ltr">This is the artifact accompanying the study of compatibility issues in theorem provers, accepted for presentation at the ACM International Conference on the Foundations of Software Engineering (FSE) 2025. This artifact includes both the colle...

Full description

Saved in:
Bibliographic Details
Main Author: Xiaokun Luan (14163030) (author)
Other Authors: David Miguel Sanan Baena (11913005) (author), Zhé Hóu (13747021) (author), Qiyuan Xu (18624037) (author), Chengwei Liu (18624039) (author), Yufan Cai (18624040) (author), Yang Liu (6089488) (author), Meng Sun (18624044) (author)
Published: 2025
Subjects:
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:<p><br></p><p dir="ltr">This is the artifact accompanying the study of compatibility issues in theorem provers, accepted for presentation at the ACM International Conference on the Foundations of Software Engineering (FSE) 2025. This artifact includes both the collected data and the reproduction package for data preparation and analysis.</p><p dir="ltr">The source code was developed by the authors of the paper. The data were collected through regression testing of different versions of the Isabelle theorem prover on the Archive of Formal Proofs (AFP), a large repository of formal proof developments. Compatibility issues were identified during this process, and relevant data were extracted and analyzed using the source code.</p>