{"id":3491,"date":"2013-08-13T05:00:48","date_gmt":"2013-08-13T05:00:48","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=3491"},"modified":"2013-08-13T05:00:48","modified_gmt":"2013-08-13T05:00:48","slug":"proof-pearl-a-verified-bignum-implementation-in-x86-64-machine-code","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/proof-pearl-a-verified-bignum-implementation-in-x86-64-machine-code\/","title":{"rendered":"Proof pearl: A verified bignum implementation in x86-64 machine code"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo de verificaci\u00f3n formal en <a href=\"http:\/\/hol.sourceforge.net\/\">HOL4<\/a> titulado <a href=\"http:\/\/www.cl.cam.ac.uk\/~mom22\/cpp13\/paper.pdf\">Proof pearl: A verified bignum implementation in x86-64 machine code<\/a>.<\/p>\n<p>Sus autores son <\/p>\n<ul>\n<li><a href=\"http:\/\/www.cl.cam.ac.uk\/~mom22\/\">Magnus O. Myreen<\/a> (de la Universidad de Cambridge)y\n<li>Gregorio Curello (de la Universidad Aut\u00f3noma de Barcelona).\n<\/ul>\n<p>Su resumen es<\/p>\n<blockquote><p>\nVerification of machine code can easily deteriorate into an endless clutter of low-level details. This paper presents a case study which shows that machine-code verification does not necessarily require ghastly low-level proofs. The case study we describe is the construction of an x86-64 implementation of arbitrary-precision integer arithmetic. Compared with closely related work, our proofs are shorter and, more importantly, the reasoning is at a more convenient high level of abstraction, e.g. pointer reasoning is largely avoided. We achieve this improvement as a result of using previously developed tools, namely, a proof-producing decompiler and compiler. The work presented in this paper has been developed in the HOL4 theorem prover and the case study resulted in 700 lines of verified 64-bit x86 machine code.\n<\/p><\/blockquote>\n<p>El c\u00f3digo correspondiente se encuentra <a href=\"http:\/\/www.cl.cam.ac.uk\/~mom22\/cpp13\/\">aqu\u00ed<\/a>.<\/p>\n<p>El trabajo se presentar\u00e1 en la <a href=\"http:\/\/cpp2013.forge.nicta.com.au\/\">CPP 2013<\/a> (<i>3rd International Conference on Certified Programs and Proofs<\/i>).<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de verificaci\u00f3n formal en HOL4 titulado Proof pearl: A verified bignum implementation in x86-64 machine code. Sus autores son Magnus O. Myreen (de la Universidad de Cambridge)y Gregorio Curello (de la Universidad Aut\u00f3noma de Barcelona). Su resumen es Verification of machine code can easily deteriorate into an endless clutter of&#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":[1],"tags":[166,199,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\/3491"}],"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=3491"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3491\/revisions"}],"predecessor-version":[{"id":3493,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3491\/revisions\/3493"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=3491"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=3491"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=3491"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}