2026-08-17T03:58:06Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:24622 2025-12-12T15:10:04Z ddc:004 open_access

Formally Verifying a Vertical Cell Decomposition Algorithm Bertot, Yves Portet, Thomas Formal Verification Motion planning algorithmic geometry 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Yves Bertot and Thomas Portet 2025 Is Part Of LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ITP.2025.24 urn:nbn:de:0030-drops-246222 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.24 eng https://creativecommons.org/licenses/by/4.0/legalcode