{"id":65205,"date":"2018-03-09T22:53:17","date_gmt":"2018-03-09T22:53:17","guid":{"rendered":"https:\/\/www.deberes.net\/tesis\/sin-categoria\/analisis-y-verificacion-de-programas-modulares\/"},"modified":"2018-03-09T22:53:17","modified_gmt":"2018-03-09T22:53:17","slug":"analisis-y-verificacion-de-programas-modulares","status":"publish","type":"post","link":"https:\/\/www.deberes.net\/tesis\/inteligencia-artificial\/analisis-y-verificacion-de-programas-modulares\/","title":{"rendered":"An\u00e1lisis y verificaci\u00f3n de programas modulares"},"content":{"rendered":"<h2>Tesis doctoral de <strong> Jes\u00fas Correas Fern\u00e1ndez <\/strong><\/h2>\n<p>Existe un gran n\u00famero de t\u00e9cnicas avanzadas de verificaci\u00f3n y optimizaci\u00f3n est\u00e1tica de programas que han demostrado ser extremadamente \u00fatiles en la detecci\u00f3n de errores de programaci\u00f3n y en la mejora de la eficiencia, y que tienen como factor com\u00fan la necesidad de informaci\u00f3n precisa de an\u00e1lisis global del programa. La interpretaci\u00f3n abstracta es una de las t\u00e9cnicas de an\u00e1lisis m\u00e1s establecidas, lo que ha permitido el desarrollo de m\u00e9todos innovadores para la verificaci\u00f3n de programas. por otra parte, uno de los desaf\u00edos m\u00e1s importantes en la investigaci\u00f3n inform\u00e1tica actual consiste en mejorar la capacidad de detectar autom\u00e1ticamente errores en programas y asegurar que un programa es correcto respecto a una determinada especificaci\u00f3n, con el objetivo de producir software. Por ello, la verificaci\u00f3n de programas es un \u00e1rea importante de investigaci\u00f3n, y por ello proporcionar t\u00e9cnicas avanzadas para detectar errores y verificar sistemas en programas reales complejos es una de las \u00e1reas m\u00e1s relevantes en la industria inform\u00e1tica actual. Un enfoque interesante de la verificaci\u00f3n de programas es la denominada verificaci\u00f3n abstracta, una t\u00e9cnica que tiene como objetivo la verificaci\u00f3n de un programa mediante sobre-aproximaciones de la sem\u00e1ntica concreta del programa. sin embargo, estos m\u00e9todos no son directamente aplicables a programas reales, pues t\u00e9cnicas avanzadas como las mencionadas est\u00e1n en muchos casos disponibles como prototipos, y los avances conseguidos hasta ahora en esta direcci\u00f3n solamente han permitido su aplicaci\u00f3n de modo restringido. el objetivo de esta tesis doctoral es desarrollar t\u00e9cnicas de an\u00e1lisis y verificaci\u00f3n para su uso eficiente y preciso en grandes programas modulares o incompletos y mostrar su factibilidad en sistemas reales. Con el fin de evaluar la utilidad pr\u00e1ctica de las t\u00e9cnicas propuestas, los algoritmos resultantes han sido implementados e integrados en el sistema ciao y se han comprobado experimentalmente, lo que ha permitido aplicarlos en casos de estudio reales.<\/p>\n<p>&nbsp;<\/p>\n<h3>Datos acad\u00e9micos de la tesis doctoral \u00ab<strong>An\u00e1lisis y verificaci\u00f3n de programas modulares<\/strong>\u00ab<\/h3>\n<ul>\n<li><strong>T\u00edtulo de la tesis:<\/strong>\u00a0 An\u00e1lisis y verificaci\u00f3n de programas modulares <\/li>\n<li><strong>Autor:<\/strong>\u00a0 Jes\u00fas Correas Fern\u00e1ndez <\/li>\n<li><strong>Universidad:<\/strong>\u00a0 Polit\u00e9cnica de Madrid<\/li>\n<li><strong>Fecha de lectura de la tesis:<\/strong>\u00a0 13\/06\/2008<\/li>\n<\/ul>\n<p>&nbsp;<\/p>\n<h3>Direcci\u00f3n y tribunal<\/h3>\n<ul>\n<li><strong>Director de la tesis<\/strong>\n<ul>\n<li>Germ\u00e1n Puebla S\u00e1nchez<\/li>\n<\/ul>\n<\/li>\n<li><strong>Tribunal<\/strong>\n<ul>\n<li>Presidente del tribunal: manuel Hermenegildo salinas <\/li>\n<li>andrew King (vocal)<\/li>\n<li>germ\u00e1n Francisco Vidal oriola (vocal)<\/li>\n<li>ricardo Pe\u00f1a mar\u00ed (vocal)<\/li>\n<\/ul>\n<\/li>\n<\/ul>\n<p>&nbsp;<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Tesis doctoral de Jes\u00fas Correas Fern\u00e1ndez Existe un gran n\u00famero de t\u00e9cnicas avanzadas de verificaci\u00f3n y optimizaci\u00f3n est\u00e1tica de programas [&hellip;]<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"site-sidebar-layout":"default","site-content-layout":"","ast-site-content-layout":"","site-content-style":"default","site-sidebar-style":"default","ast-global-header-display":"","ast-banner-title-visibility":"","ast-main-header-display":"","ast-hfb-above-header-display":"","ast-hfb-below-header-display":"","ast-hfb-mobile-header-display":"","site-post-title":"","ast-breadcrumbs-content":"","ast-featured-img":"","footer-sml-layout":"","theme-transparent-header-meta":"","adv-header-id-meta":"","stick-header-meta":"","header-above-stick-meta":"","header-main-stick-meta":"","header-below-stick-meta":"","astra-migrate-meta-layouts":"default","ast-page-background-enabled":"default","ast-page-background-meta":{"desktop":{"background-color":"var(--ast-global-color-4)","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-gradient":""},"tablet":{"background-color":"","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-gradient":""},"mobile":{"background-color":"","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-gradient":""}},"ast-content-background-meta":{"desktop":{"background-color":"var(--ast-global-color-5)","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-gradient":""},"tablet":{"background-color":"var(--ast-global-color-5)","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-gradient":""},"mobile":{"background-color":"var(--ast-global-color-5)","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-gradient":""}},"footnotes":""},"categories":[2528,6474,16008],"tags":[127894,143822,127893,143821,4816,16545],"class_list":["post-65205","post","type-post","status-publish","format-standard","hentry","category-inteligencia-artificial","category-lenguajes-de-programacion","category-politecnica-de-madrid","tag-andrew-king","tag-german-francisco-vidal-oriola","tag-german-puebla-sanchez","tag-jesus-correas-fernandez","tag-manuel-hermenegildo-salinas","tag-ricardo-pena-mari"],"_links":{"self":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/posts\/65205","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/comments?post=65205"}],"version-history":[{"count":0,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/posts\/65205\/revisions"}],"wp:attachment":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/media?parent=65205"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/categories?post=65205"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/tags?post=65205"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}