{"id":4770,"date":"2015-02-17T09:24:53","date_gmt":"2015-02-17T08:24:53","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=4770"},"modified":"2015-02-17T09:24:53","modified_gmt":"2015-02-17T08:24:53","slug":"resena-isabelle-and-security","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-isabelle-and-security\/","title":{"rendered":"Rese\u00f1a: Isabelle and security"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo sobre verifiaci\u00f3n formal con Isabelle\/HOL titulado <a href=\"http:\/\/www21.in.tum.de\/~blanchet\/iandsec.pdf\">Isabelle and security<\/a><\/p>\n<p>Sus autores son<\/p>\n<ul>\n<li><a href=\"http:\/\/www21.in.tum.de\/~blanchet\">Jasmin Christian Blanchette<\/a> (del grupo <a href=\"http:\/\/veridis.loria.fr\">VeriDis (Verification of Distributed Systems)<\/a> en el Inria Nancy &amp; LORIA y del grupo <a href=\"http:\/\/www.mpi-inf.mpg.de\/de\/departments\/automation-of-logic\">Automation of Logic<\/a> en el <em>Max Planck Institute for Informatics<\/em> de Saarbr\u00fccken) y<\/li>\n<li><a href=\"http:\/\/www.eis.mdx.ac.uk\/staffpages\/andreipopescu\">Andrei Popescu<\/a> (del grupo <a href=\"http:\/\/www.cs.mdx.ac.uk\/foundations\">Foundations of Computing<\/a> en la <em>Middlesex University London<\/em>).<\/li>\n<\/ul>\n<p>Su resumen es<\/p>\n<blockquote><p>\n  Isabelle\/HOL is a general-purpose proof assistant based on higher-order logic. Its main strengths are its simple-yet-expressive logic and its proof automation. Security researchers make up a significant fraction of Isabelle\u2019s users. In the past few years, many exciting developments have taken place, connecting programming languages, operating system kernels, and security.\n<\/p><\/blockquote>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo sobre verifiaci\u00f3n formal con Isabelle\/HOL titulado Isabelle and security Sus autores son Jasmin Christian Blanchette (del grupo VeriDis (Verification of Distributed Systems) en el Inria Nancy &amp; LORIA y del grupo Automation of Logic en el Max Planck Institute for Informatics de Saarbr\u00fccken) y Andrei Popescu (del grupo Foundations of&#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\/4770"}],"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=4770"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4770\/revisions"}],"predecessor-version":[{"id":4771,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4770\/revisions\/4771"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=4770"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=4770"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=4770"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}