DROPS

Artifact

Software

DOI: 10.4230/artifacts.24678

math-comp trajectories

Authors: Yves Bertot and Thomas Portet

Abstract

Cite as

Yves Bertot, Thomas Portet. math-comp trajectories (Software). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@misc{suppl_material,
   title = {{math-comp trajectories}}, 
   author = {Bertot, Yves and Portet, Thomas},
   note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:169acc62d26af37f236ba047dc5b75b7cc68fadb;origin=https://github.com/math-comp/trajectories;visit=swh:1:snp:6281f4cd4361a2b27e4d3dbd240f501f358e9adc;anchor=swh:1:rev:31e3a5cb7fbc46dc1ebcc988cee711a0bb01fc53}{\texttt{swh:1:dir:169acc62d26af37f236ba047dc5b75b7cc68fadb}} (visited on 2025-09-22)},
   url = {https://github.com/math-comp/trajectories/tree/vertical-cells-paper},
   doi = {10.4230/artifacts.24678},
}

Document

DOI: 10.4230/LIPIcs.ITP.2025.24

Formally Verifying a Vertical Cell Decomposition Algorithm

Authors: Yves Bertot and Thomas Portet

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

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

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)

Copy BibTex To Clipboard

@InProceedings{bertot_et_al:LIPIcs.ITP.2025.24,
  author =	{Bertot, Yves and Portet, Thomas},
  title =	{{Formally Verifying a Vertical Cell Decomposition Algorithm}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{24:1--24:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.24},
  URN =		{urn:nbn:de:0030-drops-246222},
  doi =		{10.4230/LIPIcs.ITP.2025.24},
  annote =	{Keywords: Formal Verification, Motion planning, algorithmic geometry}
}

Search Results

Documents authored by Portet, Thomas

math-comp trajectories

Abstract

Cite as

Formally Verifying a Vertical Cell Decomposition Algorithm

Abstract

Cite as

Thanks for your feedback!

Could not send message