{"id":2132,"date":"2012-08-18T08:04:19","date_gmt":"2012-08-18T08:04:19","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=2132"},"modified":"2013-03-08T05:48:13","modified_gmt":"2013-03-08T05:48:13","slug":"correctness-of-pointer-manipulating-algorithms-illustrated-by-a-verified-bdd-construction","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/correctness-of-pointer-manipulating-algorithms-illustrated-by-a-verified-bdd-construction\/","title":{"rendered":"Rese\u00f1a: Correctness of pointer manipulating algorithms illustrated by a verified BDD construction"},"content":{"rendered":"<p>Se ha publicado un nuevo trabajo de verificaci\u00f3n formal en <a href=\"http:\/\/www.cl.cam.ac.uk\/research\/hvg\/isabelle\">Isabelle\/HOL<\/a> titulado <a href=\"http:\/\/www.irit.fr\/~Mathieu.Giorgino\/Publications\/pdfs\/GiSt2012BDD.pdf\">Correctness of pointer manipulating algorithms illustrated by a verified BDD construction<\/a>.<\/p>\n<p>Los autores del trabajo son <a href=\"http:\/\/www.irit.fr\/~Mathieu.Giorgino\">Mathieu Giorgino<\/a> y <a href=\"http:\/\/www.irit.fr\/~Martin.Strecker\">Martin Strecker<\/a> (de la Univ. de Toulouse).<\/p>\n<p>El trabajo se presentar\u00e1 el 29 de agosto en el <a href=\"http:\/\/fm2012.cnam.fr\">FM 2012<\/a> (18th International Symposium on Formal Methods).<\/p>\n<p>En el trabajo se presenta una metodolog\u00eda para la verificaci\u00f3n de programas imperativos usando el asistente de prueba <a href=\"http:\/\/www.cl.cam.ac.uk\/research\/hvg\/isabelle\">Isabelle\/HOL<\/a> y su extensi\u00f3n <a href=\"http:\/\/www4.in.tum.de\/~krauss\/imperative\/imperative.pdf\">Imperative_HOL<\/a>, junto con el generador de c\u00f3digo Scala de Isabelle. Como aplicaci\u00f3n de la metodolog\u00eda se verifica los <a href=\"http:\/\/en.wikipedia.org\/wiki\/Binary_decision_diagram\">diagramas de decisi\u00f3n binarios (BDD)<\/a>.<\/p>\n<p>Su resumen es<\/p>\n<blockquote><p>\nThis paper is an extended case study using a high-level approach to the verification of graph transformation algorithms: To represent sharing, graphs are considered as trees with additional pointers, and algorithms manipulating them are essentially primitive recursive traversals written in a monadic style. With this, we achieve almost trivial termination arguments and can use inductive reasoning principles for showing the correctness of the algorithms. We illustrate the approach with the verification of a BDD package which is modular in that it can be instantiated with different implementations of association tables for node lookup. We have also implemented a garbage collector for freeing association tables from unused entries. Even without low-level optimizations, the resulting implementation is reasonably efficient. <\/p><\/blockquote>\n<p>El c\u00f3digo de la formalizaci\u00f3n se encuentra en <a href=\"http:\/\/www.irit.fr\/~Mathieu.Giorgino\/Publications\/files\/BDD_isabelle2011.tar.gz\">aqu\u00ed<\/a> <\/p>\n<p>El trabajo es parte del proyecto <a href=\"http:\/\/climt.imag.fr\">CLIMT<\/a> (Categorical and Logical Methods in Model Transformation).<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un nuevo trabajo de verificaci\u00f3n formal en Isabelle\/HOL titulado Correctness of pointer manipulating algorithms illustrated by a verified BDD construction. Los autores del trabajo son Mathieu Giorgino y Martin Strecker (de la Univ. de Toulouse). El trabajo se presentar\u00e1 el 29 de agosto en el FM 2012 (18th International Symposium on Formal&#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":[144,285,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\/2132"}],"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=2132"}],"version-history":[{"count":4,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/2132\/revisions"}],"predecessor-version":[{"id":2793,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/2132\/revisions\/2793"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=2132"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=2132"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=2132"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}