Formally verifying a vertical cell decomposition algorithm

DOI10.4230/LIPICS.ITP.2025.24MaRDI QIDQ7323675zbMATH OpenFDO

Authors Yves Bertot, Thomas Portet

Publication date 1 September 2026

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.4230/LIPICS.ITP.2025.24

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• A formally verified motion planner for autonomous vehicles
• Axioms and hulls
• Designing and proving correct a convex hull algorithm with hypermaps in Coq
• Fast formal proof of the Erdős-Szekeres conjecture for convex polygons with at most 6 points
• Formal verification of the empty hexagon number
• scientific article; zbMATH DE number 2003158 (Why is no real title available?)
• scientific article; zbMATH DE number 1863395 (Why is no real title available?)
• ROSCoq: robots powered by constructive reals
• Safe smooth paths between straight line obstacles

This page was built for publication: Formally verifying a vertical cell decomposition algorithm

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q7323675)