2 Search Results for "Tovar, Benjamin"

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.06421.7
Extracting Visibility Information by Following Walls

Authors: Anna Yershova, Benjamin Tovar, and Steven M. LaValle

Published in: Dagstuhl Seminar Proceedings, Volume 6421, Robot Navigation (2007)

Abstract
This paper presents an analysis of a simple robot model, called Bitbot. The Bitbot has limited capabilities; it can reliably follow walls and sense a contact with a wall. Although the Bitbot does not have a range sensor or a camera, it is able to acquire visibility information from the environment, which is then used to solve a pursuit-evasion task. Our developments are centered on the characterization of the information the Bitbot acquires. At any given moment, due to the sensing uncertainty, the robot does not know the current state. In general, uncertainty in the state is one of the central issues in robotics; the Bitbot model serves as an example of how the notion of information space naturally handles uncertainty. We show that state estimation with the Bitbot is a challenging problem, related to the well-known open problem of characterizing visibility graphs in computational geometry. However, state estimation becomes unnecessary to the achievement of the Bitbot's visibility tasks. We show how pursuit-evasion strategy is derived from a careful manipulation with histories of observations, and present analysis of the algorithm and experimental results.
Cite as

Anna Yershova, Benjamin Tovar, and Steven M. LaValle. Extracting Visibility Information by Following Walls. In Robot Navigation. Dagstuhl Seminar Proceedings, Volume 6421, pp. 1-18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)

Copy BibTex To Clipboard

@InProceedings{yershova_et_al:DagSemProc.06421.7,
  author =	{Yershova, Anna and Tovar, Benjamin and LaValle, Steven M.},
  title =	{{Extracting Visibility Information by Following Walls}},
  booktitle =	{Robot Navigation},
  pages =	{1--18},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2007},
  volume =	{6421},
  editor =	{S\'{a}ndor Fekete and Rudolf Fleischer and Rolf Klein and Alejandro Lopez-Ortiz},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.06421.7},
  URN =		{urn:nbn:de:0030-drops-8678},
  doi =		{10.4230/DagSemProc.06421.7},
  annote =	{Keywords: Planning, localization, pursuit evasion, visibility}
}
  • Refine by Type
  • 2 Document/PDF
  • 1 Document/HTML

  • Refine by Publication Year
  • 1 2025
  • 1 2007

  • Refine by Author
  • 1 Ghanbari, Ali
  • 1 LaValle, Steven M.
  • 1 Tovar, Benjamin
  • 1 Yershova, Anna

  • Refine by Series/Journal
  • 1 LIPIcs
  • 1 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
  • 1 Clone Detection
  • 1 Gallina
  • 1 Goal
  • 1 Planning
  • 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