{"id":4695,"date":"2015-01-05T07:34:01","date_gmt":"2015-01-05T06:34:01","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=4695"},"modified":"2015-01-05T07:34:01","modified_gmt":"2015-01-05T06:34:01","slug":"resena-a-framework-for-verified-depth-first-algorithms","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-a-framework-for-verified-depth-first-algorithms\/","title":{"rendered":"Rese\u00f1a: A framework for verified depth-first algorithms"},"content":{"rendered":"<p>En el <a href=\"http:\/\/bit.ly\/1Ae8Kq9\">CPP 2015<\/a> Peter Lammich y Ren\u00e9 Neumann presentar\u00e1n el trabajo <a href=\"http:\/\/bit.ly\/1Ae9xaP\">A framework for verifying depth-first search algorithms<\/a> que est\u00e1 basado en el de Ren\u00e9 Neumann titulado <a href=\"http:\/\/bit.ly\/1Bg6hJ4\">A framework for verified depth-first algorithms<\/a>.<\/p>\n<p>El resumen de este \u00faltimo es<\/p>\n<blockquote><p>\n  We present a framework in Isabelle\/HOL for formalizing variants of depth-first search. This framework allows to easily prove non-trivial properties of these variants. Moreover, verified code in several programming languages including Haskell, Scala and Standard ML can be generated. In this paper, we present an abstract formalization of depth-first search and demonstrate how it is refined to an efficiently executable version. Further we use the emptiness-problem of B\u00fcchi-automata known from model checking as the motivation to present three Nested DFS algorithms. They are formalized, verified and transformed into executable code using our framework.\n<\/p><\/blockquote>\n<p>El c\u00f3digo de las correspondientes teor\u00edas en Isabelle\/HOL se encuentra <a href=\"https:\/\/cava.in.tum.de\/downloads\">aqu\u00ed<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>En el CPP 2015 Peter Lammich y Ren\u00e9 Neumann presentar\u00e1n el trabajo A framework for verifying depth-first search algorithms que est\u00e1 basado en el de Ren\u00e9 Neumann titulado A framework for verified depth-first algorithms. El resumen de este \u00faltimo es We present a framework in Isabelle\/HOL for formalizing variants of depth-first search. This framework allows&#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":[144,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\/4695"}],"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=4695"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4695\/revisions"}],"predecessor-version":[{"id":4696,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4695\/revisions\/4696"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=4695"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=4695"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=4695"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}