{"id":25978,"date":"2018-03-09T09:17:35","date_gmt":"2018-03-09T09:17:35","guid":{"rendered":"https:\/\/www.deberes.net\/tesis\/sin-categoria\/especificacion-y-verificacion-de-programas-moleculares-en-pvs\/"},"modified":"2018-03-09T09:17:35","modified_gmt":"2018-03-09T09:17:35","slug":"especificacion-y-verificacion-de-programas-moleculares-en-pvs","status":"publish","type":"post","link":"https:\/\/www.deberes.net\/tesis\/sevilla\/especificacion-y-verificacion-de-programas-moleculares-en-pvs\/","title":{"rendered":"Especificaci\u00f3n y verificaci\u00f3n de programas moleculares en pvs"},"content":{"rendered":"<h2>Tesis doctoral de <strong>  Graciani D\u00edaz M. Carmen <\/strong><\/h2>\n<p>La computaci\u00f3n molecular y, en concreto, la computaci\u00f3n con adn, es una disciplina que se enmarca dentro del campo de investigaci\u00f3n conocido como computaci\u00f3n natural. Tiene como objetivo el desarrollo de modelos de computaci\u00f3n inspirados en el comportamiento de las mol\u00e9culas de adn, y en las posibilidades que abren las t\u00e9cnicas de laboratorio para su manipulaci\u00f3n.  en la memoria se han estudiado distintas adaptaciones del marco formal en que se describen distintos modelos de computaci\u00f3n con adn al lenguaje de especificaciones de pvs, que es un sistema de verificaci\u00f3n cuyo lenguaje est\u00e1 basado en la l\u00f3gica cl\u00e1sica de segundo orden con un sistema de tipos acorde con la teor\u00eda de conjuntos de zermelo-fraenkel con el axioma de elecci\u00f3n. El demostrador del sistema est\u00e1 basado en c\u00e1lculos de secuentes combinando la interacci\u00f3n con el usuario y el automatismo.  como aportaciones originales se\u00f1alar la descripci\u00f3n en pvs del modelo restringido de adleman y el modelo sticker, y la representaci\u00f3n y verificaci\u00f3n en pvs de programas moleculares que resuelven problemas cl\u00e1sicos np-completos.  en una primera aproximaci\u00f3n al modelo sticker  se ha realizado una implementaci\u00f3n de la metodolog\u00eda presentada por fernando sancho en su tesis doctoral para la verificaci\u00f3n de programas en el citado modelo. As\u00ed mismo, la consideraci\u00f3n de los programas en este modelo como meros programas imperativos ha llevado a la descripci\u00f3n de la l\u00f3gica de  primer orden para dos tipos (indpendiente de la del sistema) y del c\u00e1lculo de floyd-hoare, desarrollando un conjunto de estrategias que permiten simi-automatizar el proceso de verificaci\u00f3n de programas imperativos.  el desarrollo del trabajo ha llevado tambi\u00e9n a la elaboraci\u00f3n de un conjunto de teor\u00edas que permiten mejorar de forma natural y eficiente distintas estructuras de datos como son: multiconjuntos de elementos, conjuntos finitos de n\u00fameros naturales y aplicaciones sobre los mism<\/p>\n<p>&nbsp;<\/p>\n<h3>Datos acad\u00e9micos de la tesis doctoral \u00ab<strong>Especificaci\u00f3n y verificaci\u00f3n de programas moleculares en pvs<\/strong>\u00ab<\/h3>\n<ul>\n<li><strong>T\u00edtulo de la tesis:<\/strong>\u00a0 Especificaci\u00f3n y verificaci\u00f3n de programas moleculares en pvs <\/li>\n<li><strong>Autor:<\/strong>\u00a0  Graciani D\u00edaz M. Carmen <\/li>\n<li><strong>Universidad:<\/strong>\u00a0 Sevilla<\/li>\n<li><strong>Fecha de lectura de la tesis:<\/strong>\u00a0 29\/09\/2003<\/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> P\u00e9rez Jim\u00e9nez Mario Jes\u00fas<\/li>\n<\/ul>\n<\/li>\n<li><strong>Tribunal<\/strong>\n<ul>\n<li>Presidente del tribunal: eladio Dom\u00ednguez murillo <\/li>\n<li> Castellano pe\u00f1uela Juan  bautista (vocal)<\/li>\n<li>Jos\u00e9 Antonio Alonso jimenez (vocal)<\/li>\n<li> Rosell\u00f3 llompart francesc andreu (vocal)<\/li>\n<\/ul>\n<\/li>\n<\/ul>\n<p>&nbsp;<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Tesis doctoral de Graciani D\u00edaz M. Carmen La computaci\u00f3n molecular y, en concreto, la computaci\u00f3n con adn, es una disciplina [&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":[10715],"tags":[75390,10833,75389,10822,55578,75391],"class_list":["post-25978","post","type-post","status-publish","format-standard","hentry","category-sevilla","tag-castellano-penuela-juan-bautista","tag-eladio-dominguez-murillo","tag-graciani-diaz-m-carmen","tag-jose-antonio-alonso-jimenez","tag-perez-jimenez-mario-jesus","tag-rosello-llompart-francesc-andreu"],"_links":{"self":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/posts\/25978","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=25978"}],"version-history":[{"count":0,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/posts\/25978\/revisions"}],"wp:attachment":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/media?parent=25978"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/categories?post=25978"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/tags?post=25978"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}