{"id":488,"date":"2010-08-31T14:27:26","date_gmt":"2010-08-31T14:27:26","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/premios-hvc-de-verificacion-a-la-comunidad-smt-satisfiability-modulo-theories\/"},"modified":"2013-03-08T05:53:41","modified_gmt":"2013-03-08T05:53:41","slug":"premios-hvc-de-verificacion-a-la-comunidad-smt-satisfiability-modulo-theories","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/premios-hvc-de-verificacion-a-la-comunidad-smt-satisfiability-modulo-theories\/","title":{"rendered":"Premios HVC de verificaci\u00f3n a la comunidad SMT (Satisfiability Modulo Theories)"},"content":{"rendered":"<p>\nLos premios HVC (Haifa Verification Conference) se conceden a los trabajos m\u00e1s prometedores en la campos de verificaci\u00f3n y prueba de software y hardware. Este a\u00f1o <a href=\"http:\/\/researchweb.watson.ibm.com\/haifa\/conferences\/hvc2010\/award.shtml\">los premios HVC 2010<\/a> le han sido otorgados a los promotores de la comunidad de <a href=\"http:\/\/en.wikipedia.org\/wiki\/Satisfiability_Modulo_Theories\">satisfacibilidad m\u00f3dulo teor\u00edas<\/a> (en ingl\u00e9s, <i>Satisfiability Modulo Theories (SMT<\/i>) personalisados en<\/p>\n<ul>\n<li><a href=\"http:\/\/www.cs.uiowa.edu\/~astump\/\">Clark Barrett<\/a> (Universidad de New York),\n<li><a href=\"http:\/\/research.microsoft.com\/en-us\/um\/people\/leonardo\/\">Leonardo De-Moura (Microsoft Research),\n<li><a href=\"http:\/\/www.loria.fr\/~ranise\/\">Silvio Ranise<\/a> (INRIA),\n<li><a href=\"http:\/\/www.cs.uiowa.edu\/~astump\/\">Aaron Stump<\/a> (Universidad de Iowa) y\n<li><a href=\"http:\/\/www.cs.uiowa.edu\/~tinelli\/\">Cesare Tinelli<\/a> (Universidad de Iowa).\n<\/ul>\n<p><!--more--><\/p>\n<p>\nCon el premio se reconoce el papel que han jugado en la creaci\u00f3n y promoci\u00f3n de la comunidad SMT, principalmente con los siguientes proyectos:<\/p>\n<ul>\n<li>el <a href=\"http:\/\/combination.cs.uiowa.edu\/smtlib\/papers\/pdpar-proposal.pdf\">formato SMT-lib<\/a> definido por Ranise y Tinelli como un lenguaje com\u00fan para especificar pruebas para SMT. La <a href=\"http:\/\/combination.cs.uiowa.edu\/smtlib\/papers\/smt-lib-reference-v2.0-r10.08.28.pdf\">vesi\u00f3n actual<\/a> es obra de  Barrett, Stump y Tinelli.\n<li>el <a href=\"http:\/\/smtexec.org\/exec\/smtlib-portal-benchmarks.php\"> repositorio SMT-LIB<\/a> en el que se recopilan pruebas para SMT. Actualmente contiene 93.480 pruebas. Los principales gestores del repositorio son Barrett, Deters y Tinelli.\n<li>la <a heref=\"http:\/\/combination.cs.uiowa.edu\/smtlib\/competition.html\"> competici\u00f3n SMT-COMP<\/a> en la que compiten anualmente sistemas SMT. Los actuales organizadores son Clark Barrett, Morgan Deters, Albert Oliveras y Aaron Stump.\n<li>el <a href=\"http:\/\/www.smtexec.org\/\">SMT-Exec<\/a> (The Satisfiability Modulo Theories Execution Service) que es un servicio web que permite realizar experimentos en l\u00ednea son sistemas SMT sobre las pruebas de SMT-lib. Los promotores de SMT-Exec son Deters y Stump.\n<\/ul>\n<p>\nAdem\u00e1s, se reconoce el \u00e9xito acad\u00e9mico e industrial dee la satisfacibilidad m\u00f3dulo teor\u00eda. El \u00e9xito acad\u00e9mico de SMT puede apreciarse en los art\u00edculos publicados. Actualmente se encuentran <a href=\"http:\/\/scholar.google.es\/scholar?as_q=&#038;num=10&#038;btnG=Buscar+en+Google+Acad%C3%A9mico&#038;as_epq=%22Satisfiability+modulo+theories%22&#038;as_oq=&#038;as_eq=&#038;as_occt=any&#038;as_sauthors=&#038;as_publication=&#038;as_ylo=&#038;as_yhi=&#038;hl=es\">1100 art\u00edculos<\/a> en Google Scholar al buscar &#8220;Satisfiability modulo theories&#8221;. El \u00e9xito industrial de SMT puede apreciarse en las empresas que usan sistemas SMT. <\/p>\n<ul>\n<li> Microsoft usa el <a href=\"http:\/\/research.microsoft.com\/projects\/z3\">Z3<\/a> en herramientas de an\u00e1lisis de programas,\n<li> Intel usa <a href=\"http:\/\/mathsat.fbk.eu\/\">MathSAT<\/a> y <a href=\"http:\/\/fmv.jku.at\/boolector\/\">Boolector<\/a> para la verificaci\u00f3n de hardware,\n<li> otras empresas que usan sistema SMT son Galois Connection, Praxis, GrammaTech, NVIDIA, Synopsys , Mathworks, Dassault Aviation, etc.\n<\/ul>\n<p>\nLos sistemas SMT se est\u00e1n integrando en los demostradores de teoremas. Por ejemplo, <a href=\"http:\/\/www.cl.cam.ac.uk\/research\/hvg\/isabelle\/\">Isabelle<\/a> integra <a href=\"http:\/\/research.microsoft.com\/projects\/z3\">Z3<\/a> y <a href=\"http:\/\/pvs.csl.sri.com\/\">PVS<\/a> integra <a href=\"http:\/\/yices.csl.sri.com\/\">Yices<\/a>.<\/p>\n<p>\nUna buena introducci\u00f3n a la satisfacibilidad m\u00f3dulo teor\u00edas es el cap\u00edtulo de Clark Barrett, Roberto Sebastiani, Sanjit Seshia y Cesare Tinelli <a href=\"ftp:\/\/ftp.cs.uiowa.edu\/pub\/tinelli\/papers\/BarSST-09.pdf\">Satisfiability Modulo Theories<\/a> en el <a href=\"http:\/\/www.st.ewi.tudelft.nl\/sat\/handbook\/\">Handbook on Satisfiability<\/a> (IOS Press, Febrero de 2009). <\/p>\n","protected":false},"excerpt":{"rendered":"<p>Los premios HVC (Haifa Verification Conference) se conceden a los trabajos m\u00e1s prometedores en la campos de verificaci\u00f3n y prueba de software y hardware. Este a\u00f1o los premios HVC 2010 le han sido otorgados a los promotores de la comunidad de satisfacibilidad m\u00f3dulo teor\u00edas (en ingl\u00e9s, Satisfiability Modulo Theories (SMT) personalisados en Clark Barrett (Universidad&#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":[1],"tags":[110,114,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\/488"}],"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=488"}],"version-history":[{"count":6,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/488\/revisions"}],"predecessor-version":[{"id":3025,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/488\/revisions\/3025"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=488"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=488"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=488"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}