2026-07-21T20:03:26Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:26654 2026-07-13T14:00:37Z ddc:004 open_access

End-to-End Certified Graph Colouring Dold, Simon Katsirelos, George Koops, Wietze Myreen, Magnus O. Nordström, Jakob Oertel, Andy Tan, Yong Kiam graph colouring proof logging certifying algorithms Applied combinatorial optimization has witnessed a revolution in performance since the turn of the millennium, but the complexity of modern solvers is making bugs an ever more serious concern. The most promising remedy is to make solvers certifying, so that they use proof logging to generate machine-verifiable proofs of correctness. We present the first example of state-of-the-art certified graph colouring by equipping the solver ZykovColor with VeriPB proof logging. Combined with the formally verified CakePB checker, this provides end-to-end formally certified results. An experimental evaluation shows excellent results with only moderate overhead for proof logging and checking. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Simon Dold and George Katsirelos and Wietze Koops and Magnus O. Myreen and Jakob Nordström and Andy Oertel and Yong Kiam Tan 2026 Is Part Of LIPIcs, Volume 379, 32nd International Conference on Principles and Practice of Constraint Programming (CP 2026) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CP.2026.21 urn:nbn:de:0030-drops-266546 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2026.21 eng https://creativecommons.org/licenses/by/4.0/legalcode