{"id":3899,"date":"2013-12-08T05:30:30","date_gmt":"2013-12-08T04:30:30","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=3899"},"modified":"2013-12-07T08:15:07","modified_gmt":"2013-12-07T07:15:07","slug":"applications-of-interactive-proof-to-data-flow-analysis-and-security","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/applications-of-interactive-proof-to-data-flow-analysis-and-security\/","title":{"rendered":"Applications of interactive proof to data flow analysis and security"},"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> sobre sem\u00e1ntica de lenguajes de programaci\u00f3n titulado <a href=\"http:\/\/www.nicta.com.au\/pub?doc=7256\">Applications of interactive proof to data flow analysis and security<\/a>.<\/p>\n<p>Sus autores son <\/p>\n<ul>\n<li> <a href=\"http:\/\/www.cse.unsw.edu.au\/~kleing\">Gerwin Klein<\/a> (del NICTA, Australia).\n<li> <a href=\"http:\/\/www21.in.tum.de\/~nipkow\/\">Tobias Nipkow<\/a> (de la Univ. T\u00e9cnica de Munich, Alemania) y\n<\/ul>\n<p>Su resumen es<\/p>\n<blockquote><p>\nWe show how to formalise a small imperative programming language in the theorem prover Isabelle\/HOL, how to define its semantics, and how to prove properties about the language, its type systems, and a number of data flow analyses. <\/p>\n<p>The emphasis is not on formalising a complex language deeply, but to teach a number of formalisation techniques and proof strategies using simple examples. For this purpose, we cover a basic type system with type safety proof, more complex security type systems, also with soundness proofs, and different kinds of data flow analyses, in particular definite initialisation analysis and constant propagation, again with correctness proofs.\n<\/p><\/blockquote>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en Isabelle\/HOL sobre sem\u00e1ntica de lenguajes de programaci\u00f3n titulado Applications of interactive proof to data flow analysis and security. Sus autores son Gerwin Klein (del NICTA, Australia). Tobias Nipkow (de la Univ. T\u00e9cnica de Munich, Alemania) y Su resumen es We show how to formalise a small&#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\/3899"}],"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=3899"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3899\/revisions"}],"predecessor-version":[{"id":3901,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3899\/revisions\/3901"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=3899"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=3899"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=3899"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}