{"id":3452,"date":"2013-07-28T05:25:10","date_gmt":"2013-07-28T05:25:10","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=3452"},"modified":"2013-07-28T05:25:10","modified_gmt":"2013-07-28T05:25:10","slug":"resena-program-verification-based-on-kleene-algebra-in-isabellehol","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-program-verification-based-on-kleene-algebra-in-isabellehol\/","title":{"rendered":"Rese\u00f1a: Program verification based on Kleene algebra in Isabelle\/HOL"},"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> titulado <a href=\"http:\/\/staffwww.dcs.shef.ac.uk\/people\/A.Armstrong\/skat\/paper.pdf\">Program verification based on Kleene algebra in Isabelle\/HOL<\/a>.<\/p>\n<p>Sus autores son <a href=\"http:\/\/staffwww.dcs.shef.ac.uk\/people\/A.Armstrong\/\">Alasdair Armstrong<\/a>, <a href=\"http:\/\/staffwww.dcs.shef.ac.uk\/people\/G.Struth\">Georg Struth<\/a> y <a href=\"http:\/\/user.it.uu.se\/~tjawe125\">Tjark Weber<\/a> (los dos primeros de la Universidad de Sheffield y el tercero de la de Uppsala).<\/p>\n<p>El trabajo se ha presentado esta semana en el <a href=\"http:\/\/itp2013.inria.fr\">ITP 2013<\/a> (<i>4th Conference on<br \/>\nInteractive Theorem Proving<\/i>). <\/p>\n<p>Su resumen es<\/p>\n<blockquote><p>\nSchematic Kleene algebra with tests (SKAT) supports the equational verification of flowchart scheme equivalence and captures simple while programs with assignment statements. We formalise SKAT in Isabelle\/HOL, using the quotient type package to reason equationally in this algebra. We apply this formalisation to a complex flowchart transformation proof from the literature. We extend SKAT with assertion statements and derive the inference rules of Hoare logic. We apply this extension in simple program verification examples and the derivation of additional Hoare-style rules. This shows that algebra can provide an abstract semantic layer from which different program analysis and verification tasks can be implemented in a simple lightweight way.\n<\/p><\/blockquote>\n<p>El c\u00f3digo de las correspondientes teor\u00edas en Isabelle\/HOL se encuentra <a href=\"http:\/\/staffwww.dcs.shef.ac.uk\/people\/A.Armstrong\/skat\/skat.tgz\">aqu\u00ed<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en Isabelle\/HOL titulado Program verification based on Kleene algebra in Isabelle\/HOL. Sus autores son Alasdair Armstrong, Georg Struth y Tjark Weber (los dos primeros de la Universidad de Sheffield y el tercero de la de Uppsala). El trabajo se ha presentado esta semana en el ITP 2013&#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":[1],"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\/3452"}],"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=3452"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3452\/revisions"}],"predecessor-version":[{"id":3453,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3452\/revisions\/3453"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=3452"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=3452"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=3452"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}