{"id":3238,"date":"2013-04-19T06:14:13","date_gmt":"2013-04-19T06:14:13","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=3238"},"modified":"2013-04-19T06:14:13","modified_gmt":"2013-04-19T06:14:13","slug":"resena-formalization-of-incremental-simplex-algorithm-by-stepwise-refinement","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-formalization-of-incremental-simplex-algorithm-by-stepwise-refinement\/","title":{"rendered":"Rese\u00f1a: Formalization of incremental simplex algorithm by stepwise refinement"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en <a href=\"http:\/\/www.cl.cam.ac.uk\/research\/hvg\/Isabelle\/index.html\">Isabelle\/HOL<\/a> titulado <a href=\"http:\/\/argo.matf.bg.ac.rs\/publications\/2012\/simplex.pdf\">Formalization of incremental simplex algorithm by stepwise refinement<\/a>.<\/p>\n<p>Sus autores son <a href=\"http:\/\/poincare.matf.bg.ac.rs\/~mirko\">Mirko Spasi\u0107<\/a> and <a href=\"http:\/\/poincare.matf.bg.ac.rs\/~filip\">Filip Mari\u0107<\/a> (de la Universidad de Belgrado).<\/p>\n<p>Su resumen es<\/p>\n<blockquote><p>\nWe present an Isabelle\/HOL formalization and total correctness proof for the incremental version of the Simplex algorithm which is used in most state-of-the-art SMT solvers. Formalization relies on stepwise program and data refinement, starting from a simple specification, going through a number of fine refinement steps, and ending up in a fully executable functional implementation. Symmetries present in the algorithm are handled with special care.\n<\/p><\/blockquote>\n<p>El trabajo se present\u00f3 en el <a href=\"http:\/\/fm2012.cnam.fr\/\">FM2012<\/a> (18th International Symposium on Formal Methods) y las transparencias de la presentaci\u00f3n se encuentran <a href=\"http:\/\/argo.matf.bg.ac.rs\/publications\/2012\/simplex-fm-slides.pdf\">aqu\u00ed<\/a>.<\/p>\n<p>El c\u00f3digo de las teor\u00edas en Isabelle\/HOL se encuentran <a href=\"http:\/\/argo.matf.bg.ac.rs\/downloads\/formalizations\/Simplex.zip\">aqu\u00ed<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en Isabelle\/HOL titulado Formalization of incremental simplex algorithm by stepwise refinement. Sus autores son Mirko Spasi\u0107 and Filip Mari\u0107 (de la Universidad de Belgrado). Su resumen es We present an Isabelle\/HOL formalization and total correctness proof for the incremental version of the Simplex algorithm which is used&#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\/3238"}],"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=3238"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3238\/revisions"}],"predecessor-version":[{"id":3239,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3238\/revisions\/3239"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=3238"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=3238"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=3238"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}