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

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.

DOI10.1007/978-3-642-32759-9\_12
Citation KeySimula.simula.1322