FSE 2025
Mon 23 - Fri 27 June 2025 Trondheim, Norway
co-located with ISSTA 2025
Wed 25 Jun 2025 15:00 - 15:20 at Cosmos 3C - Empirical Studies 2 Chair(s): Yuchao Jiang

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.

Wed 25 Jun

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

14:00 - 15:30
14:00
20m
Talk
An Empirical Analysis of Issue Templates Usage in Large-Scale Projects on GitHub
Journal First
Emre Sülün Bilkent University, Metehan Saçakcı Bilkent University, Eray Tüzün Bilkent University
14:20
20m
Talk
The Landscape of Toxicity: An Empirical Investigation of Toxicity on GitHub
Research Papers
Jaydeb Sarker University of Nebraska at Omaha, Asif Kamal Turzo Wayne State University, Amiangshu Bosu Wayne State University
DOI Pre-print
14:40
20m
Talk
Expressing and Checking Statistical Assumptions
Research Papers
Alexi Turcotte CISPA, Zheyuan Wu Saarland University
DOI
15:00
20m
Talk
Why the Proof Fails in Different Versions of Theorem Provers: An Empirical Study of Compatibility Issues in Isabelle
Research Papers
Xiaokun Luan Peking University, David Sanan Singapore Institute of Technology, Zhe Hou Griffith University, Qiyuan Xu Nanyang Technological University, Chengwei Liu Nanyang Technological University, Yufan Cai National University of Singapore, Yang Liu Nanyang Technological University, Meng Sun Peking University
DOI
15:20
10m
Talk
Missing Threats: Dealing with the Treatment-sensitive Factorial Structure Bias in Empirical Software Engineering
Ideas, Visions and Reflections
Sabato Nocera University of Salerno, Giuseppe Scanniello University of Salerno

Information for Participants
Wed 25 Jun 2025 14:00 - 15:30 at Cosmos 3C - Empirical Studies 2 Chair(s): Yuchao Jiang
Info for room Cosmos 3C:

Cosmos 3C is the third room in the Cosmos 3 wing.

When facing the main Cosmos Hall, access to the Cosmos 3 wing is on the left, close to the stairs. The area is accessed through a large door with the number “3”, which will stay open during the event.

:
:
:
: