|Authors||C. Dubois and A. Gotlieb|
|Title||Towards an Effective Formally Certified Constraint Solver|
|Afilliation||Software Engineering, Software Engineering, Software Engineering|
|Project(s)||The Certus Centre (SFI)|
|Publication Type||Talks, contributed|
|Year of Publication||2014|
|Location of Talk||Selected talk at the 'Verification meets CP' 2014 workshop, Lyon, France|
When used to verify safety-critical properties of a software system, the answers provided by a CP-based constraint solver must be formally certied through trusted and faithful methodologies. In such cases, one has often to formally verify that a constraint system is unsatisable, as it is required to prove that no reachable states can violate the property to be ensured. Unfortunately, proving that a constraint system is unsatisable is much more complex for a CP-solver than checking a possible solution.