AuthorsC. Dubois and A. Gotlieb
TitleTowards an Effective Formally Certified Constraint Solver
AfilliationSoftware Engineering, Software Engineering, Software Engineering
Project(s)The Certus Centre (SFI)
StatusPublished
Publication TypeTalks, contributed
Year of Publication2014
Location of TalkSelected talk at the 'Verification meets CP' 2014 workshop, Lyon, France
Publisher.
Place Published.
KeywordsWorkshop
Abstract

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.

Citation KeySimula.simula.2856