DROPS

Document

DOI: 10.4230/LIPIcs.CP.2026.24

Formally Verified Certification of Constraint Programming Proofs

Authors: Maarten Flippo, Konstantin Sidorov, Tip ten Brink, Clément Pit-Claudel, and Emir Demirović

Published in: LIPIcs, Volume 379, 32nd International Conference on Principles and Practice of Constraint Programming (CP 2026)

Abstract

As constraint programming (CP) solvers are increasingly used in critical applications, there is a growing need for certification of solver claims of infeasibility and optimality. Recent work has demonstrated that certification is feasible for CP solvers using a multi-stage proof-generation framework; however, the underlying proof system was informal, and verification relied on translation into an external proof format, impacting the trustworthiness. We address these issues by formalising a rigorous, solver-agnostic framework for certifying CP solver claims. We present a formal definition of DRCP, a proof system for CP over integer domains that captures core solver operations, including conflict analysis and heterogeneous propagation, by modular inference rules with precise semantics. We also develop FznDrcpCheck, a formally verified proof checker in Rocq that validates DRCP proofs directly against FlatZinc models. Our evaluation shows that our framework enables practical certification across various benchmarks with negligible overhead during solving and modest proof-checking costs.

Cite as

Maarten Flippo, Konstantin Sidorov, Tip ten Brink, Clément Pit-Claudel, and Emir Demirović. Formally Verified Certification of Constraint Programming Proofs. In 32nd International Conference on Principles and Practice of Constraint Programming (CP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 379, pp. 24:1-24:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{flippo_et_al:LIPIcs.CP.2026.24,
  author =	{Flippo, Maarten and Sidorov, Konstantin and ten Brink, Tip and Pit-Claudel, Cl\'{e}ment and Demirovi\'{c}, Emir},
  title =	{{Formally Verified Certification of Constraint Programming Proofs}},
  booktitle =	{32nd International Conference on Principles and Practice of Constraint Programming (CP 2026)},
  pages =	{24:1--24:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-432-1},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{379},
  editor =	{Beldiceanu, Nicolas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2026.24},
  URN =		{urn:nbn:de:0030-drops-266560},
  doi =		{10.4230/LIPIcs.CP.2026.24},
  annote =	{Keywords: Constraint programming, Proof systems, Certified checking}
}

Search Results

Documents authored by ten Brink, Tip

Formally Verified Certification of Constraint Programming Proofs

Abstract

Cite as

Thanks for your feedback!

Could not send message