Search Results

Documents authored by Bertot, Yves

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}
}
Document
Complete Volume
DOI: 10.4230/LIPIcs.ITP.2024
LIPIcs, Volume 309, ITP 2024, Complete Volume

Authors: Yves Bertot, Temur Kutsia, and Michael Norrish

Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)

Abstract
LIPIcs, Volume 309, ITP 2024, Complete Volume
Cite as

15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 1-714, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@Proceedings{bertot_et_al:LIPIcs.ITP.2024,
  title =	{{LIPIcs, Volume 309, ITP 2024, Complete Volume}},
  booktitle =	{15th International Conference on Interactive Theorem Proving (ITP 2024)},
  pages =	{1--714},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-337-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{309},
  editor =	{Bertot, Yves and Kutsia, Temur and Norrish, Michael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024},
  URN =		{urn:nbn:de:0030-drops-207277},
  doi =		{10.4230/LIPIcs.ITP.2024},
  annote =	{Keywords: LIPIcs, Volume 309, ITP 2024, Complete Volume}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.ITP.2024.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Yves Bertot, Temur Kutsia, and Michael Norrish

Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)

Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as

15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 0:i-0:xii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{bertot_et_al:LIPIcs.ITP.2024.0,
  author =	{Bertot, Yves and Kutsia, Temur and Norrish, Michael},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{15th International Conference on Interactive Theorem Proving (ITP 2024)},
  pages =	{0:i--0:xii},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-337-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{309},
  editor =	{Bertot, Yves and Kutsia, Temur and Norrish, Michael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.0},
  URN =		{urn:nbn:de:0030-drops-207287},
  doi =		{10.4230/LIPIcs.ITP.2024.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
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