Document Open Access Logo

Formally Verifying a Vertical Cell Decomposition Algorithm

Authors Yves Bertot , Thomas Portet

PDF HTML 5

Files

Thumbnail PDF
PDF
LIPIcs.ITP.2025.24.pdf
  • Filesize: 0.88 MB
  • 18 pages
HTML5 Logo HTML (experimental)
LIPIcs.ITP.2025.24.html

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Computational geometry
  • Theory of computation → Program verification
  • Theory of computation → Higher order logic
  • Theory of computation → Logic and verification
  • Theory of computation → Type theory
Keywords
  • Formal Verification
  • Motion planning
  • algorithmic geometry

Metrics

Abstract

The broad context of this work is the application of formal methods to geometry and robotics. We describe an algorithm to decompose a working area containing obstacles into a collection of safe cells and the formal proof that this algorithm is correct. We expect such an algorithm will be useful to compute safe trajectories.
To our knowledge, this is one of the first formalization of such an algorithm to decompose a working space into elementary cells that are suitable for later applications, with the proof of correctness that guarantees that large parts of the working space are safe. Techniques to perform this proof go from algebraic reasoning on coordinates and determinants to sorting. The main difficulty comes from the possible existence of degenerate cases, which are treated in a principled way.

Cite As Get BibTex

Yves Bertot and Thomas Portet. Formally Verifying a Vertical Cell Decomposition Algorithm. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 24:1-24:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.ITP.2025.24

Author Details

Yves Bertot
  • Inria Center at Université Côte d'Azur, Nice, France
Thomas Portet
  • Inria Center at Université Côte d'Azur, Nice, France

Supplementary Materials

References

  1. Abhishek Anand and Ross Knepper. Roscoq: Robots powered by constructive reals. In Christian Urban and Xingyuan Zhang, editors, Interactive Theorem Proving, pages 34-50, Cham, 2015. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-22102-1_3.
  2. Yves Bertot. Safe smooth paths between straight line obstacles. In Venanzio Capretta, Robbert Krebbers, and Freek Wiedijk, editors, Logics and Type Systems in Theory and Practice, volume LNCS-14560 of Lecture Notes in Computer Science, pages 36-53. Springer, May 2024. URL: https://doi.org/10.1007/978-3-031-61716-4_3.
  3. Yves Bertot and Thomas Portet. supplementary material for this paper, June 2025. . . URL: https://github.com/math-comp/trajectories/tree/vertical-cells-paper
    Software Heritage Logo archived version
    full metadata available at: https://doi.org/10.4230/artifacts.24678
  4. Christophe Brun, Jean-François Dufourd, and Nicolas Magaud. Designing and proving correct a convex hull algorithm with hypermaps in Coq. Computational Geometry, 45(8):436-457, October 2012. URL: https://doi.org/10.1016/j.comgeo.2010.06.006.
  5. Fabian Immler. A verified algorithm for geometric zonotope/hyperplane intersection. In Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP '15, pages 129-136, New York, NY, USA, 2015. Association for Computing Machinery. URL: https://doi.org/10.1145/2676724.2693164.
  6. Donald Knuth. Axioms and Hulls. Number 606 in Lecture Notes in Computer Science. Springer-Verlag, 1991. URL: https://doi.org/10.1007/3-540-55611-7.
  7. Jean-Claude Latombe. Robot Motion Planning. Kluwer Academic Publishers, 1991. URL: https://doi.org/10.1007/978-1-4615-4022-9.
  8. Pierre Letouzey. A New Extraction for Coq. In Herman Geuvers and Freek Wiedijk, editors, Types for Proofs and Programs: International Workshop, TYPES 2002, Lecture Notes in Computer Science, page 617, Berg en Dal, Netherlands, February 2004. Springer. URL: https://hal.science/hal-00150914.
  9. Assia Mahboubi and Enrico Tassi. Mathematical Components. Zenodo, September 2022. URL: https://doi.org/10.5281/zenodo.7118596.
  10. Filip Marić. Fast Formal Proof of the Erdős–Szekeres Conjecture for Convex Polygons with at Most 6 Points. Journal of Automated Reasoning, 62:301-329, 2019. URL: https://doi.org/10.1007/s10817-017-9423-7.
  11. David Pichardie and Yves Bertot. Formalizing Convex Hulls Algorithms. In LNCS, volume 2152 of TPHOLs 2001: Theorem Proving in Higher Order Logics, pages 346-361, Edinburgh, United Kingdom, September 2001. Springer. URL: https://doi.org/10.1007/3-540-44755-5_24.
  12. Albert Rizaldi, Fabian Immler, Bastian Schürmann, and Matthias Althoff. A formally verified motion planner for autonomous vehicles. In Shuvendu K. Lahiri and Chao Wang, editors, Automated Technology for Verification and Analysis, pages 75-90, Cham, 2018. Springer International Publishing. URL: https://doi.org/10.1007/978-3-030-01090-4_5.
  13. Bernardo Subercaseaux, Wojciech Nawrocki, James Gallicchio, Cayden Codel, Mario Carneiro, and Marijn J. H. Heule. Formal Verification of the Empty Hexagon Number. In Yves Bertot, Temur Kutsia, and Michael Norrish, editors, 15th International Conference on Interactive Theorem Proving (ITP 2024), volume 309 of Leibniz International Proceedings in Informatics (LIPIcs), pages 35:1-35:19, Dagstuhl, Germany, 2024. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ITP.2024.35.
  14. The Rocq Development Team. The rocq prover, April 2025. URL: https://doi.org/10.5281/zenodo.15149629.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact