{"id":5454,"date":"2016-05-27T06:00:34","date_gmt":"2016-05-27T04:00:34","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=5454"},"modified":"2016-05-26T22:55:10","modified_gmt":"2016-05-26T20:55:10","slug":"resena-refinement-based-verification-of-imperative-data-structures","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-refinement-based-verification-of-imperative-data-structures\/","title":{"rendered":"Rese\u00f1a: Refinement based verification of imperative data structures"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en <a href=\"http:\/\/www.cl.cam.ac.uk\/research\/hvg\/Isabelle\/index.html\">Isabelle\/HOL<\/a> sobre algor\u00edtmica titulado <a href=\"https:\/\/www21.in.tum.de\/~lammich\/pub\/cpp2016_impds.pdf\">Refinement based verification of imperative data structures<\/a><\/p>\n<p>Su autor es <a href=\"http:\/\/www21.in.tum.de\/~lammich\/\">Peter Lammich<\/a> (de la <a href=\"http:\/\/www21.in.tum.de\/\">Chair for Logic and Verification<\/a> en la Univ. t\u00e9cnica de Munich).<\/p>\n<p>Su resumen es<\/p>\n<blockquote><p>\n  In this paper we present a stepwise refinement based top-down approach to verified imperative data structures. Our approach is modular in the sense that already verified data structures can be used for construction of more complex data structures. Moreover, our data structures can be used as building blocks for the verification of algorithms. Our tool chain supports refinement down to executable code in various programming languages, and is fully implemented in Isabelle\/HOL, such that its trusted code base is only the inference kernel and the code generator of Isabelle\/HOL.<\/p>\n<p>  As a case study, we verify an indexed heap data structure, and use it to generate an efficient verified implementation of Dijkstra\u2019s algorithm.\n<\/p><\/blockquote>\n<p>El trabajo se ha presentado en el <a href=\"https:\/\/people.csail.mit.edu\/adamc\/cpp16\/index.html\u00baq\">CPP 2016<\/a> (<em>The 5th ACM SIGPLAN Conference on Certified Programs and Proofs<\/em>).<\/p>\n<p>El c\u00f3digo de las correspondientes teor\u00edas en Isabelle\/HOL se encuentra <a href=\"http:\/\/www21.in.tum.de\/~lammich\/heapmaps\/\">aqu\u00ed<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en Isabelle\/HOL sobre algor\u00edtmica titulado Refinement based verification of imperative data structures Su autor es Peter Lammich (de la Chair for Logic and Verification en la Univ. t\u00e9cnica de Munich). Su resumen es In this paper we present a stepwise refinement based top-down approach to verified imperative&#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],"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\/5454"}],"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=5454"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/5454\/revisions"}],"predecessor-version":[{"id":5455,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/5454\/revisions\/5455"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=5454"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=5454"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=5454"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}