{"id":2266,"date":"2012-11-07T07:14:50","date_gmt":"2012-11-07T07:14:50","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=2266"},"modified":"2013-03-08T05:47:40","modified_gmt":"2013-03-08T05:47:40","slug":"contributions-a-la-verification-formelle-dalgorithmes-arithmetiques","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/contributions-a-la-verification-formelle-dalgorithmes-arithmetiques\/","title":{"rendered":"Rese\u00f1a: Contributions to the formal verification of arithmetic algorithms"},"content":{"rendered":"<p>El pasado mes de septiembre se present\u00f3 una tesis sobre verificaci\u00f3n formal con <a href=\"http:\/\/coq.inria.fr\/\">Coq<\/a> titulada <a href=\"http:\/\/erik.martin-dorel.org\/papers\/MARTIN-DOREL_Erik_2012_these.pdf\">Contributions to the formal verification of arithmetic algorithms<\/a>.<\/p>\n<p>Su autor es <a href=\"http:\/\/erik.martin-dorel.org\/\">\u00c9rik Martin-Dorel<\/a>, dirigido por <a href=\"http:\/\/www-lipn.univ-paris13.fr\/~mayero\/\">Micaela Mayero<\/a> y <a href=\"http:\/\/perso.ens-lyon.fr\/jean-michel.muller\/\">Jean-Michel Muller<\/a>.  <\/p>\n<p>Su resumen es<\/p>\n<blockquote><p>\nThe Floating-Point (FP) implementation of a real-valued function is performed with correct rounding if the output is always equal to the rounding of the exact value, which has many advantages. But for implementing a function with correct rounding in a reliable and efficient manner, one has to solve the &#8220;Table Maker&#8217;s Dilemma&#8221; (TMD). Two sophisticated algorithms (L and SLZ) have been designed to solve this problem, relying on some long and complex calculations that are performed by some heavily-optimized implementations. Hence the motivation to provide strong guarantees on these costly pre-computations. To this end, we use the Coq proof assistant. First, we develop a library of &#8220;Rigorous Polynomial Approximation&#8221;, allowing one to compute an approximation polynomial and an interval that bounds the approximation error in Coq. This formalization is a key building block for verifying the first step of SLZ, as well as the implementation of a mathematical function in general (with or without correct rounding). Then we have implemented, formally verified and made effective 3 interrelated certificates checkers in Coq, whose correctness proof derives from Hensel&#8217;s lemma that we have formalized for both univariate and bivariate cases. In particular, our &#8220;ISValP verifier&#8221; is a key component for formally verifying the results generated by SLZ. Then, we have focused on the mathematical proof of &#8220;augmented-precision&#8221; FP algorithms for the square root and the Euclidean 2D norm. We give some tight lower bounds on the minimum non-zero distance between sqrt(x\u00b2+y\u00b2) and a midpoint, allowing one to solve the TMD for this bivariate function. Finally, the &#8220;double-rounding&#8221; phenomenon can typically occur when several FP precision are available, and may change the behavior of some usual small FP algorithms. We have formally verified in Coq a set of results describing the behavior of the Fast2Sum algorithm with double-roundings.\n<\/p><\/blockquote>\n<p>Las transparencias usadas en la presentaci\u00f3n se encuentran <a href=\"http:\/\/erik.martin-dorel.org\/slides\/MARTIN-DOREL_Erik_2012_soutenance.pdf\">aqu\u00ed<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>El pasado mes de septiembre se present\u00f3 una tesis sobre verificaci\u00f3n formal con Coq titulada Contributions to the formal verification of arithmetic algorithms. Su autor es \u00c9rik Martin-Dorel, dirigido por Micaela Mayero y Jean-Michel Muller. Su resumen es The Floating-Point (FP) implementation of a real-valued function is performed with correct rounding if the output is&#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":[100],"tags":[45,285,37,275],"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\/2266"}],"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=2266"}],"version-history":[{"count":7,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/2266\/revisions"}],"predecessor-version":[{"id":2756,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/2266\/revisions\/2756"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=2266"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=2266"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=2266"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}