{"id":4765,"date":"2015-02-13T07:49:20","date_gmt":"2015-02-13T06:49:20","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=4765"},"modified":"2015-02-13T07:49:20","modified_gmt":"2015-02-13T06:49:20","slug":"resena-machine-checked-proofs-for-realizability-checking-algorithms","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-machine-checked-proofs-for-realizability-checking-algorithms\/","title":{"rendered":"Rese\u00f1a: Machine-checked proofs for realizability checking algorithms"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en Coq sobre titulado <a href=\"http:\/\/arxiv.org\/pdf\/1502.01292v1\">Machine-checked proofs for realizability checking algorithms<\/a>.<\/p>\n<p>Sus autores son<\/p>\n<ul>\n<li><a href=\"http:\/\/www.umsec.umn.edu\/directory\/Andreas-Katis\">Andreas Katis<\/a> (de la Universidad de Minesota),<\/li>\n<li><a href=\"http:\/\/loonwerks.com\/people\/andrew-gacek.html\">Andrew Gacek<\/a> (del <em>Rockwell Collins Advanced Technology Center<\/em>) y<\/li>\n<li><a href=\"http:\/\/www-users.cs.umn.edu\/~whalen\">Michael W. Whalen<\/a> (del <a href=\"http:\/\/crisys.cs.umn.edu\">Critical Systems Group (CriSys)<\/a> en la Universidad de Minesota).<\/li>\n<\/ul>\n<p>Su resumen es<\/p>\n<blockquote><p>\n  We have recently proposed a contract-based realizability checking algorithm involving the use of theories, to provide an auxiliary procedure to consistency checking of &#8220;leaf-level&#8221; components in complex embedded systems. To prove the soundness of our approach on realizability, we formalized the necessary definitions and theorems of <a href=\"http:\/\/www.umsec.umn.edu\/sites\/www.umsec.umn.edu\/files\/document.pdf\">Towards realizability checking of contracts using theories<\/a>, in the Coq proof and specification language.\n<\/p><\/blockquote>\n<p>El c\u00f3digo de las correspondientes teor\u00edas en Coq se encuentra [aqu\u00ed](.https:\/\/github.com\/andrewkatis\/Coq\/<br \/>\nblob\/master\/realizability\/Realizability.v).<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en Coq sobre titulado Machine-checked proofs for realizability checking algorithms. Sus autores son Andreas Katis (de la Universidad de Minesota), Andrew Gacek (del Rockwell Collins Advanced Technology Center) y Michael W. Whalen (del Critical Systems Group (CriSys) en la Universidad de Minesota). Su resumen es We have&#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":[45,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\/4765"}],"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=4765"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4765\/revisions"}],"predecessor-version":[{"id":4766,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4765\/revisions\/4766"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=4765"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=4765"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=4765"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}