{"id":3439,"date":"2013-07-12T06:04:41","date_gmt":"2013-07-12T06:04:41","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=3439"},"modified":"2013-07-12T06:04:41","modified_gmt":"2013-07-12T06:04:41","slug":"resena-computational-verification-of-network-programs-in-coq","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-computational-verification-of-network-programs-in-coq\/","title":{"rendered":"Rese\u00f1a: &#8220;Computational verification of network programs in Coq&#8221;"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo de verificaci\u00f3n formal en <a href=\"http:\/\/coq.inria.fr\/\">Coq<\/a> titulado <a href=\"http:\/\/www.cs.princeton.edu\/~jsseven\/papers\/netcorewp\/paper.pdf\">Computational verification of network programs in Coq<\/a>.<\/p>\n<p>Su autor es <a href=\"http:\/\/www.cs.princeton.edu\/~jsseven\/\">Gordon Stewart<\/a> (miembro del proyecto <a href=\"http:\/\/vst.cs.princeton.edu\/\">Verified Software Toolchain<\/a> la Universidad de Princeton).<\/p>\n<p>Su resumen es <\/p>\n<blockquote><p>\nWe report on the design of the first fully automatic, machine-checked tool suite for verification of high-level network programs. The tool suite targets programs written in NetCore, a new declarative network programming language. Our work builds on a recent effort by Guha, Reitblatt, and Foster to build a machine-verified compiler from NetCore to OpenFlow, a new protocol for software-defined networking. The result is an end-to-end system that provides strong guarantees on the compiled OpenFlow flow tables that are installed on actual network switches.\n<\/p><\/blockquote>\n<p>El correspondiente c\u00f3digo en Coq se encuentra <a href=\"http:\/\/www.cs.princeton.edu\/~jsseven\/papers\/netcorewp\/\">aqu\u00ed<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de verificaci\u00f3n formal en Coq titulado Computational verification of network programs in Coq. Su autor es Gordon Stewart (miembro del proyecto Verified Software Toolchain la Universidad de Princeton). Su resumen es We report on the design of the first fully automatic, machine-checked tool suite for verification of high-level network programs&#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":[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\/3439"}],"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=3439"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3439\/revisions"}],"predecessor-version":[{"id":3440,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3439\/revisions\/3440"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=3439"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=3439"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=3439"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}