{"id":3883,"date":"2013-12-05T06:54:04","date_gmt":"2013-12-05T05:54:04","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=3883"},"modified":"2013-12-05T06:54:04","modified_gmt":"2013-12-05T05:54:04","slug":"formalizing-probabilistic-noninterference","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/formalizing-probabilistic-noninterference\/","title":{"rendered":"Formalizing probabilistic noninterference"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en <a href=\"http:\/\/www.cl.cam.ac.uk\/research\/hvg\/Isabelle\">Isabelle\/HOL<\/a> titulado <a href=\"http:\/\/www21.in.tum.de\/~popescua\/pdf\/PROB.pdf\">Formalizing probabilistic noninterference<\/a><\/p>\n<p>Sus autores son <a href=\"http:\/\/www21.in.tum.de\/~popescua\">Andrei Popescu<\/a>, <a href=\"http:\/\/home.in.tum.de\/~hoelzl\">Johannes H\u00f6lzl<\/a> y <a href=\"http:\/\/www21.in.tum.de\/~nipkow\/\">Tobias Nipkow<\/a> (de la Universidad T\u00e9cnica de Munich, Alemania).<\/p>\n<p>Su resumen es<\/p>\n<blockquote><p>\nWe present an Isabelle formalization of probabilistic noninterference for a multi-threaded language with uniform scheduling. Unlike in previous settings from the literature, here probabilistic behavior comes from both the scheduler and the individual threads, making the language more realistic and the mathematics more challenging. We study resumption-based and trace-based notions of probabilistic noninterference and their relationship, and also discuss compositionality w.r.t. the language constructs and type-system-like syntactic criteria. The formalization uses recent development in the Isabelle probability theory library.\n<\/p><\/blockquote>\n<p>El trabajo se presentar\u00e1 en el <a href=\"http:\/\/cpp2013.forge.nicta.com.au\/\">CPP 2013<\/a> (<i>3rd International Conference on Certified Programs and Proofs<\/i>).<\/p>\n<p>El c\u00f3digo de las correspondientes teor\u00edas en Isabelle se encuentra <a href=\"http:\/\/www21.in.tum.de\/~popescua\/prob.zip\">aqu\u00ed<\/a>. <\/p>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en Isabelle\/HOL titulado Formalizing probabilistic noninterference Sus autores son Andrei Popescu, Johannes H\u00f6lzl y Tobias Nipkow (de la Universidad T\u00e9cnica de Munich, Alemania). Su resumen es We present an Isabelle formalization of probabilistic noninterference for a multi-threaded language with uniform scheduling. Unlike in previous settings from the&#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":[85,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\/3883"}],"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=3883"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3883\/revisions"}],"predecessor-version":[{"id":3884,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3883\/revisions\/3884"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=3883"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=3883"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=3883"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}