AuthorsC. Dubois and A. Gotlieb
EditorsD. M. D. Giannakopoulou
TitleA Certified Constraint Solver Over Finite Domains
AfilliationSoftware Engineering, Software Engineering, Software Engineering
Project(s)The Certus Centre (SFI)
Publication TypeProceedings, refereed
Year of Publication2012
Conference NameProceedings of Formal Methods (FM'12), Paris, Aug. 2012
Date PublishedAugust
PublisherSpringer Berlin Heidelberg
Place PublishedBerlin Heidelberg

Constraint programs such as those written in modern Constraint Programming languages and platforms aim at solving problems coming from optimization, scheduling, planning, etc. Recently CP programs 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 answer saying that a safety property is satisfied while there exist counterexamples. In this paper, we present a Coq formalization of a constraint filtering algorithm - AC3 and one of its variant AC2001 - and a simple 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.

Citation KeySimula.simula.1322