{"id":483,"date":"2010-08-30T08:49:40","date_gmt":"2010-08-30T08:49:40","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/anuncio-trace-based-verification-of-imperative-programs-with-iotrace-based-verification-of-imperative-programs-with-io\/"},"modified":"2013-03-08T05:53:41","modified_gmt":"2013-03-08T05:53:41","slug":"anuncio-trace-based-verification-of-imperative-programs-with-io","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/anuncio-trace-based-verification-of-imperative-programs-with-io\/","title":{"rendered":"Anuncio: Trace-based verification of imperative programs with I\/O"},"content":{"rendered":"<p>\n<a href\"http:\/\/www.people.fas.harvard.edu\/~gmalecha\/\">Gregory Malecha<\/a>, <a href=\"http:\/\/www.eecs.harvard.edu\/~greg\/\">Greg Morrisett<\/a> y <a href=\"http:\/\/www.eecs.harvard.edu\/~ryan\/\">Ryan Wisnesky<\/a> han publicado el art\u00edculo <a href=\"http:\/\/www.sciencedirect.com\/science?_ob=ArticleURL&#038;_udi=B6WM7-50W80T2-2&#038;_user=10&#038;_coverDate=08\/27\/2010&#038;_rdoc=1&#038;_fmt=high&#038;_orig=search&#038;_origin=search&#038;_sort=d&#038;_docanchor=&#038;view=c&#038;_acct=C000050221&#038;_version=1&#038;_urlVersion=0&#038;_userid=10&#038;md5=028d486d3366332b873fc26e37373497&#038;searchtype=a\">Trace-based verification of imperative programs with I\/O<\/a> en el <i>Journal of Symbolic Computation<\/i>. Una versi\u00f3n del art\u00edculo puede leerse <a href=\"http:\/\/www.eecs.harvard.edu\/~ryan\/jscwwv10.pdf\">aqu\u00ed<\/a>.<\/p>\n<p>\nEl resumen del art\u00edculo es<\/p>\n<blockquote><p>\nIn this paper we demonstrate how to prove the correctness of systems implemented using low-level imperative features like pointers, files, and socket I\/O with respect to high level I\/O protocol descriptions by using <a href=\"http:\/\/coq.inria.fr\/\">the Coq proof assistant<\/a>. We present a web-based course gradebook application developed with <a href=\"http:\/\/ynot.cs.harvard.edu\/\">Ynot<\/a>, a Coq library for verified imperative programming. We add a dialog-based I\/O system to Ynot, and we extend Ynot\u2019s underlying Hoare logic with event traces to reason about I\/O and protocol behavior. Expressive abstractions allow the modular verification of both high level specifications like privacy guarantees and low level properties like data structure pointer invariants.\n<\/p><\/blockquote>\n<p>\nLos autores son miembros del <a href=\"http:\/\/cs.harvard.edu\/pl\">Grupo de Lenguajes de Programaci\u00f3n<\/a> de la <a href=\"http:\/\/es.wikipedia.org\/wiki\/Universidad_Harvard\">Universidad de Harvard<\/a>.<\/p>\n<p>\nEste  art\u00edculo est\u00e1 relacionado con el proyecto SAFE (Semantically Aware Foundation Environment) comentado en una <a href=\"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/trabajo-de-logica-computacional-en-las-universidades-de-pensilvania-harvard-y-northeastern\/\">entrada anterior<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Gregory Malecha, Greg Morrisett y Ryan Wisnesky han publicado el art\u00edculo Trace-based verification of imperative programs with I\/O en el Journal of Symbolic Computation. Una versi\u00f3n del art\u00edculo puede leerse aqu\u00ed. El resumen del art\u00edculo es In this paper we demonstrate how to prove the correctness of systems implemented using low-level imperative features like pointers,&#8230;<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"closed","ping_status":"closed","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":[20,45,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\/483"}],"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=483"}],"version-history":[{"count":5,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/483\/revisions"}],"predecessor-version":[{"id":3026,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/483\/revisions\/3026"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=483"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=483"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=483"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}