{"id":4963,"date":"2015-08-12T08:43:02","date_gmt":"2015-08-12T06:43:02","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=4963"},"modified":"2015-08-12T08:43:02","modified_gmt":"2015-08-12T06:43:02","slug":"resena-formal-verification-of-programs-computing-the-floating-point-average","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-formal-verification-of-programs-computing-the-floating-point-average\/","title":{"rendered":"Rese\u00f1a: Formal verification of programs computing the floating-point average"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en <a href=\"https:\/\/coq.inria.fr\/\">Coq<\/a> sobre la aritm\u00e9tica titulado <a href=\"https:\/\/hal.inria.fr\/hal-01174892\/document\">Formal verification of programs computing the floating-point average<\/a>.<\/p>\n<p>Sus autora es <a href=\"https:\/\/www.lri.fr\/~sboldo\/\">Silvie Boldo<\/a> (del grupo <a href=\"http:\/\/toccata.lri.fr\">Toccata (Formally Verified Programs, Certified Tools and Numerical Computations)<\/a> en el LRI (Laboratoire de Recherche en Informatique) de la Universidad Paris-Sur).<\/p>\n<p>Su resumen es<\/p>\n<blockquote><p>\n  The most well-known feature of floating-point arithmetic is the limited precision, which creates round-off errors and inaccuracies. Another important issue is the limited range, which creates underflow and overflow, even if this topic is dismissed most of the time. This article shows a very simple example: the average of two floating-point numbers. As we want to take exceptional behaviors into account, we cannot use the naive formula (x+y)\/2. Based on hints given by Sterbenz, we first write an accurate program and formally prove its properties. An interesting fact is that Sterbenz did not give this program, but only specified it. We prove this specification and include a new property: a precise certified error bound. We also present and formally prove a new algorithm that computes the correct rounding of the average of two floating-point numbers. It is more accurate than the previous one and is correct whatever the inputs.\n<\/p><\/blockquote>\n<p>El trabajo se presentar\u00e1 en el <a href=\"http:\/\/icfem2015.lri.fr\">ICFEM 2015 (The 17th International Conference on Formal Engineering Methods)<\/a>.<\/p>\n<p>El c\u00f3digo de las correspondientes teor\u00edas en Coq se encuentra <a href=\"https:\/\/www.lri.fr\/~sboldo\/research\">aqu\u00ed<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en Coq sobre la aritm\u00e9tica titulado Formal verification of programs computing the floating-point average. Sus autora es Silvie Boldo (del grupo Toccata (Formally Verified Programs, Certified Tools and Numerical Computations) en el LRI (Laboratoire de Recherche en Informatique) de la Universidad Paris-Sur). Su resumen es The most&#8230;<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"open","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],"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\/4963"}],"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=4963"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4963\/revisions"}],"predecessor-version":[{"id":4964,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4963\/revisions\/4964"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=4963"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=4963"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=4963"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}