{"id":2072,"date":"2012-06-18T05:12:37","date_gmt":"2012-06-18T05:12:37","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=2072"},"modified":"2013-03-08T05:48:14","modified_gmt":"2013-03-08T05:48:14","slug":"resena-large-scale-formal-verification-in-practice-a-process-perspective","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-large-scale-formal-verification-in-practice-a-process-perspective\/","title":{"rendered":"Rese\u00f1a: Large-scale formal verification in practice: A process perspective"},"content":{"rendered":"<p>Una de los proyectos m\u00e1s importante en verificaci\u00f3n formal es el <a href=\"http:\/\/www.ertos.nicta.com.au\/research\/sel4\/\">seL4 (Secure Microkernel Project)<\/a> cuyo objetivo es la verificaci\u00f3n con Isabelle\/HOL del <a href=\"http:\/\/es.wikipedia.org\/wiki\/L4_(micron\u00facleo)\">micron\u00facleo<\/a> de S.O. seL4.<\/p>\n<p>El 7 de junio, se present\u00f3 en el <a href=\"http:\/\/www.ifi.uzh.ch\/icse2012\">ICSE 2012<\/a> (34th International Conference on Software Engineering) un panorama del proyecto sel4: <a href=\"http:\/\/www.nicta.com.au\/pub?id=5396\">Large-scale formal verification in practice: A process perspective<\/a>.<\/p>\n<p>Sus autores son June Andronick, Ross Jeffery, Gerwin Klein, Rafal Kolanski, Mark Staples, He (Jason) Zhang y Liming Zhu del <a href=\"http:\/\/www.nicta.com.au\">NICTA (National ICT Australia Ltd)<\/a>.<\/p>\n<p>Su resumen es<\/p>\n<blockquote><p>\nThe L4 verified project was a rare success in large-scale, formal verification: it provided a formal, machine-checked, code-level proof of the full functional correctness of the seL4 microkernel. In this paper we report on the development process and management issues of this project, highlighting key success factors. We formulate a detailed descriptive model of its middle-out development process, and analyze the evolution and dependencies of code and proof artifacts. We compare our key findings on verification and re-verification with insights from other verification efforts in the literature. Our analysis of the project is based on complete access to project logs, meeting notes, and version control data over its entire history, including its long-term, ongoing maintenance phase. The aim of this work is to aid understanding of how to successfully run large-scale formal software verification projects.\n<\/p><\/blockquote>\n","protected":false},"excerpt":{"rendered":"<p>Una de los proyectos m\u00e1s importante en verificaci\u00f3n formal es el seL4 (Secure Microkernel Project) cuyo objetivo es la verificaci\u00f3n con Isabelle\/HOL del micron\u00facleo de S.O. seL4. El 7 de junio, se present\u00f3 en el ICSE 2012 (34th International Conference on Software Engineering) un panorama del proyecto sel4: Large-scale formal verification in practice: A process&#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":[100],"tags":[144,285,275],"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\/2072"}],"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=2072"}],"version-history":[{"count":3,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/2072\/revisions"}],"predecessor-version":[{"id":2811,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/2072\/revisions\/2811"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=2072"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=2072"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=2072"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}