3 Search Results for "Kapser, Cory"

Document
DOI: 10.4230/LIPIcs.ECOOP.2025.12
Automatic Goal Clone Detection in Rocq

Authors: Ali Ghanbari

Published in: LIPIcs, Volume 333, 39th European Conference on Object-Oriented Programming (ECOOP 2025)

Abstract
Proof engineering in Rocq is a labor-intensive process, and as proof developments grow in size, redundancy and maintainability become challenges. One such redundancy is goal cloning, i.e., proving α-equivalent goals multiple times, leading to wasted effort and bloated proof scripts. In this paper, we introduce clone-finder, a novel technique for detecting goal clones in Rocq proofs. By leveraging the formal notion of α-equivalence for Gallina terms, clone-finder systematically identifies duplicated proof goals across large Rocq codebases. We evaluate clone-finder on 40 real-world Rocq projects from the CoqGym dataset. Our results reveal that each project contains an average of 27.73 instances of goal clone. We observed that the clones can be categorized as either exact goal duplication, generalization, or α-equivalent goals with different proofs, each signifying varying levels duplicate effort. Our findings highlight significant untapped potential for proof reuse in Rocq-based formal verification projects, paving the way for future improvements in automated proof engineering.
Cite as

Ali Ghanbari. Automatic Goal Clone Detection in Rocq. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 12:1-12:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{ghanbari:LIPIcs.ECOOP.2025.12,
  author =	{Ghanbari, Ali},
  title =	{{Automatic Goal Clone Detection in Rocq}},
  booktitle =	{39th European Conference on Object-Oriented Programming (ECOOP 2025)},
  pages =	{12:1--12:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-373-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{333},
  editor =	{Aldrich, Jonathan and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2025.12},
  URN =		{urn:nbn:de:0030-drops-233055},
  doi =		{10.4230/LIPIcs.ECOOP.2025.12},
  annote =	{Keywords: Clone Detection, Goal, Proof, Rocq, Gallina}
}
Document
DOI: 10.4230/DagSemProc.06301.3
06301 Working Session Summary: Presentation and Visualization of Redundant Code

Authors: Andrew Walenstein, James R. Cordy, William S. Evans, Ahmed Hassan, Toshihiro Kamiya, Cory Kapser, and Ettore Merlo

Published in: Dagstuhl Seminar Proceedings, Volume 6301, Duplication, Redundancy, and Similarity in Software (2007)

Abstract
This report summarizes the proceedings of a workshop discussion session presentation and visualization of aspects relating to duplicated, copied, or cloned code. The main outcomes of the working session were: (a) a realization that two researchers had independently generated very similar methods for browsing and visualization clone "clusters," and (b) a list of questions for visualization, particularly in relation to how the "proximity" of clones may relate to interest in the clone.
Cite as

Andrew Walenstein, James R. Cordy, William S. Evans, Ahmed Hassan, Toshihiro Kamiya, Cory Kapser, and Ettore Merlo. 06301 Working Session Summary: Presentation and Visualization of Redundant Code. In Duplication, Redundancy, and Similarity in Software. Dagstuhl Seminar Proceedings, Volume 6301, pp. 1-5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)

Copy BibTex To Clipboard

@InProceedings{walenstein_et_al:DagSemProc.06301.3,
  author =	{Walenstein, Andrew and Cordy, James R. and Evans, William S. and Hassan, Ahmed and Kamiya, Toshihiro and Kapser, Cory and Merlo, Ettore},
  title =	{{06301 Working Session Summary: Presentation and Visualization of Redundant Code}},
  booktitle =	{Duplication, Redundancy, and Similarity in Software},
  pages =	{1--5},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2007},
  volume =	{6301},
  editor =	{Rainer Koschke and Ettore Merlo and Andrew Walenstein},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.06301.3},
  URN =		{urn:nbn:de:0030-drops-9661},
  doi =		{10.4230/DagSemProc.06301.3},
  annote =	{Keywords: Code clone, clone visualization, presentation, software visualization}
}
Document
DOI: 10.4230/DagSemProc.06301.12
Subjectivity in Clone Judgment: Can We Ever Agree?

Authors: Cory Kapser, Paul Anderson, Michael Godfrey, Rainer Koschke, Matthias Rieger, Filip van Rysselberghe, and Peter Weißgerber

Published in: Dagstuhl Seminar Proceedings, Volume 6301, Duplication, Redundancy, and Similarity in Software (2007)

Abstract
An objective definition of what a code clone is currently eludes the field. A small study was performed at an international workshop to elicit judgments and discussions from world experts regarding what characteristics define a code clone. Less than half of the clone candidates judged had 80% agreement amongst the judges. Judges appeared to differ primarily in their criteria for judgment rather than their interpretation of the clone candidates. In subsequent open discussion the judges provided several reasons for their judgments. The study casts additional doubt on the reliability of experimental results in the field when the full criterion for clone judgment is not spelled out.
Cite as

Cory Kapser, Paul Anderson, Michael Godfrey, Rainer Koschke, Matthias Rieger, Filip van Rysselberghe, and Peter Weißgerber. Subjectivity in Clone Judgment: Can We Ever Agree?. In Duplication, Redundancy, and Similarity in Software. Dagstuhl Seminar Proceedings, Volume 6301, pp. 1-5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)

Copy BibTex To Clipboard

@InProceedings{kapser_et_al:DagSemProc.06301.12,
  author =	{Kapser, Cory and Anderson, Paul and Godfrey, Michael and Koschke, Rainer and Rieger, Matthias and van Rysselberghe, Filip and Wei{\ss}gerber, Peter},
  title =	{{Subjectivity in Clone Judgment:  Can We Ever Agree?}},
  booktitle =	{Duplication, Redundancy, and Similarity in Software},
  pages =	{1--5},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2007},
  volume =	{6301},
  editor =	{Rainer Koschke and Ettore Merlo and Andrew Walenstein},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.06301.12},
  URN =		{urn:nbn:de:0030-drops-9701},
  doi =		{10.4230/DagSemProc.06301.12},
  annote =	{Keywords: Code clone, study, inter-rater agreement, ill-defined problem}
}
  • Refine by Type
  • 3 Document/PDF
  • 1 Document/HTML

  • Refine by Publication Year
  • 1 2025
  • 2 2007

  • Refine by Author
  • 2 Kapser, Cory
  • 1 Anderson, Paul
  • 1 Cordy, James R.
  • 1 Evans, William S.
  • 1 Ghanbari, Ali
  • Show More...

  • Refine by Series/Journal
  • 1 LIPIcs
  • 2 DagSemProc

  • Refine by Classification
  • 1 Software and its engineering → Formal software verification
  • 1 Software and its engineering → Software maintenance tools
  • 1 Theory of computation → Type theory

  • Refine by Keyword
  • 2 Code clone
  • 1 Clone Detection
  • 1 Gallina
  • 1 Goal
  • 1 Proof
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact