{"id":3484,"date":"2013-08-09T23:17:47","date_gmt":"2013-08-09T23:17:47","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=3484"},"modified":"2013-08-09T16:20:33","modified_gmt":"2013-08-09T16:20:33","slug":"proving-soundness-of-combinatorial-vickrey-auctions-and-generating-verified-executable-code","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/proving-soundness-of-combinatorial-vickrey-auctions-and-generating-verified-executable-code\/","title":{"rendered":"Proving soundness of combinatorial Vickrey auctions and generating verified executable code"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en <a href=\"http:\/\/www.cl.cam.ac.uk\/research\/hvg\/Isabelle\/\">Isabelle\/HOL<\/a> titulado <a href=\"http:\/\/arxiv.org\/pdf\/1308.1779v1\">Proving soundness of combinatorial Vickrey auctions and generating verified executable code<\/a>.<\/p>\n<p>Sus autores son <\/p>\n<ul>\n<li><a href=\"https:\/\/sites.google.com\/site\/marcocaminati\/\">Marco B. Caminati<\/a> (de la Universidad de Roma),\n<li><a href=\"http:\/\/www.cs.bham.ac.uk\/~mmk\/\">Manfred Kerber<\/a> (de la Universidad de Birmingham),\n<li><a href=\"http:\/\/www.cs.bham.ac.uk\/~langec\/\">Christoph Lange<\/a> (de la Universidad de Birmingham) y\n<li><a href=\"http:\/\/www.socscistaff.bham.ac.uk\/rowat\/\">Colin Rowat<\/a> (de la Universidad de Birmingham).\n<\/ul>\n<p>Su resumen es<\/p>\n<blockquote><p>\nUsing mechanised reasoning we prove that combinatorial Vickrey auctions are soundly specified in that they associate a unique outcome (allocation and transfers) to any valid input (bids). Having done so, we auto-generate verified executable code from the formally defined auction. This removes a source of error in implementing the auction design. We intend to use formal methods to verify new auction designs. Here, our contribution is to introduce and demonstrate the use of formal methods for auction verification in the familiar setting of a well-known auction.\n<\/p><\/blockquote>\n<p>El trabajo se ha desarrollado como parte del proyecto <a href=\"http:\/\/www.cs.bham.ac.uk\/research\/projects\/formare\/\">ForMaRE<\/a> (<i>Formal Mathematical Reasoning in Economics<\/i>). <\/p>\n<p>El c\u00f3digo de las correspondientes teor\u00edas en Isabelle se encuentra <a href=\"http:\/\/www.cs.bham.ac.uk\/research\/projects\/formare\/code\/auction-theory\/isabelle\/\">aqu\u00ed<\/a>. <\/p>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en Isabelle\/HOL titulado Proving soundness of combinatorial Vickrey auctions and generating verified executable code. Sus autores son Marco B. Caminati (de la Universidad de Roma), Manfred Kerber (de la Universidad de Birmingham), Christoph Lange (de la Universidad de Birmingham) y Colin Rowat (de la Universidad de Birmingham)&#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":[144,273,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\/3484"}],"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=3484"}],"version-history":[{"count":3,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3484\/revisions"}],"predecessor-version":[{"id":3487,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3484\/revisions\/3487"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=3484"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=3484"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=3484"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}