A certified constraint solver over finite domains

Constraint programs such as those written in modern Con- straint Programming languages and platforms aim at solving problems coming from optimization, scheduling, planning, etc. Recently CP pro- grams have been used in business-critical or safety-critical areas as well, e.g., e-Commerce, air-traffic control applications, or software verification. This implies a more skeptical regard on the implementation of constraint solvers, especially when the result is that a constraint problem has no solution, i.e., unsatisfiability. For example, in software model checking, using an unsafe constraint solver may result in a dramatic wrong an- swer saying that a safety property is satisfied while there exist counter- examples. In this paper, we present a Coq formalization of a constraint filtering algorithm ? AC3 and one of its variant AC2001 ? and a sim- ple labeling procedure. The proof of their soundness and completeness has been completed using Coq. As a result, a formally verified constraint solver written in OCaml has been automatically extracted from the Coq specification of the filtering and labeling algorithms. The solver, yet not as efficient as specialized existing (unsafe) implementations, can be used to formally certify that a constraint system is unsatisfiable