{"id":3409,"date":"2013-06-19T04:40:32","date_gmt":"2013-06-19T04:40:32","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=3409"},"modified":"2013-06-19T04:41:10","modified_gmt":"2013-06-19T04:41:10","slug":"resena-solveurs-cpfd-verifies-formellement","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-solveurs-cpfd-verifies-formellement\/","title":{"rendered":"Rese\u00f1a: Solveurs CP(FD) v\u00e9rifi\u00e9s formellement"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en <a href=\"http:\/\/coq.inria.fr\/\">Coq<\/a> sobre restricciones titulado <a href=\"http:\/\/www.lsis.org\/jfpc-jiaf2013\/jfpc\/articles\/papier_5.pdf\">Solveurs CP(FD) v\u00e9rifi\u00e9s formellement<\/a>.<\/p>\n<p>Sus autores son <a href=\"http:\/\/www.ensiie.fr\/~dubois\/\">Catherine Dubois<\/a> y <a href=\"http:\/\/people.rennes.inria.fr\/Arnaud.Gotlieb\/\">Arnaud Gotlieb<\/a>.<\/p>\n<p>El trabajo se ha presentado en las <a href=\"http:\/\/www.lsis.org\/jfpc-jiaf2013\/jfpc\/documents\/programme.pdf\">9\u00e8mes Journ\u00e9es Francophones de Programmation par Contraintes<\/a>.<\/p>\n<p>Su resumen es<\/p>\n<blockquote><p>\nConstraint solvers are used to solve problems coming from optimization, scheduling, planning, etc. Their usage in critical applications implies a more skeptical regard on their implementation, especially when the result is that a constraint problem has no solution, i.e., unsatisfiability. In this paper, we propose an approach aiming to develop a correct-by-construction finite domain based &#8211; CP(FD) &#8211; solver. We developed this solver within the Coq proof tool and proved its correctness in Coq. It embeds the algorithm AC3 (and AC2001) and uses arc-consistency. The Coq extraction mechanism allows us to provide a finite domain based solver written in OCaml formally verified, the first one to our knowledge. This solver can be used directly or as a second shot solver to verify results coming from an untrusted solver. This result has recently been published in <a href=\"http:\/\/cedric.cnam.fr\/index.php\/publis\/article\/view?id=2547\">FM 2012<\/a>]. In this paper, we present a summary of this result and extend it to deal with another local-consistency property, namely, bound-consistency.\n<\/p><\/blockquote>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en Coq sobre restricciones titulado Solveurs CP(FD) v\u00e9rifi\u00e9s formellement. Sus autores son Catherine Dubois y Arnaud Gotlieb. El trabajo se ha presentado en las 9\u00e8mes Journ\u00e9es Francophones de Programmation par Contraintes. Su resumen es Constraint solvers are used to solve problems coming from optimization, scheduling, planning, etc&#8230;.<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"closed","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_kad_post_transparent":"","_kad_post_title":"","_kad_post_layout":"","_kad_post_sidebar_id":"","_kad_post_content_style":"","_kad_post_vertical_padding":"","_kad_post_feature":"","_kad_post_feature_position":"","_kad_post_header":false,"_kad_post_footer":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"footnotes":"","_jetpack_memberships_contains_paid_content":false},"categories":[1],"tags":[45,285],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"jetpack_likes_enabled":false,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3409"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/comments?post=3409"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3409\/revisions"}],"predecessor-version":[{"id":3411,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3409\/revisions\/3411"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=3409"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=3409"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=3409"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}