Tesis doctoral de Graciani Díaz M. Carmen
La computación molecular y, en concreto, la computación con adn, es una disciplina que se enmarca dentro del campo de investigación conocido como computación natural. Tiene como objetivo el desarrollo de modelos de computación inspirados en el comportamiento de las moléculas de adn, y en las posibilidades que abren las técnicas de laboratorio para su manipulación. en la memoria se han estudiado distintas adaptaciones del marco formal en que se describen distintos modelos de computación con adn al lenguaje de especificaciones de pvs, que es un sistema de verificación cuyo lenguaje está basado en la lógica clásica de segundo orden con un sistema de tipos acorde con la teoría de conjuntos de zermelo-fraenkel con el axioma de elección. El demostrador del sistema está basado en cálculos de secuentes combinando la interacción con el usuario y el automatismo. como aportaciones originales señalar la descripción en pvs del modelo restringido de adleman y el modelo sticker, y la representación y verificación en pvs de programas moleculares que resuelven problemas clásicos np-completos. en una primera aproximación al modelo sticker se ha realizado una implementación de la metodología presentada por fernando sancho en su tesis doctoral para la verificación de programas en el citado modelo. Así mismo, la consideración de los programas en este modelo como meros programas imperativos ha llevado a la descripción de la lógica de primer orden para dos tipos (indpendiente de la del sistema) y del cálculo de floyd-hoare, desarrollando un conjunto de estrategias que permiten simi-automatizar el proceso de verificación de programas imperativos. el desarrollo del trabajo ha llevado también a la elaboración de un conjunto de teorías que permiten mejorar de forma natural y eficiente distintas estructuras de datos como son: multiconjuntos de elementos, conjuntos finitos de números naturales y aplicaciones sobre los mism
Datos académicos de la tesis doctoral «Especificación y verificación de programas moleculares en pvs«
- Título de la tesis: Especificación y verificación de programas moleculares en pvs
- Autor: Graciani Díaz M. Carmen
- Universidad: Sevilla
- Fecha de lectura de la tesis: 29/09/2003
Dirección y tribunal
- Director de la tesis
- Pérez Jiménez Mario Jesús
- Tribunal
- Presidente del tribunal: eladio Domínguez murillo
- Castellano peñuela Juan bautista (vocal)
- José Antonio Alonso jimenez (vocal)
- Roselló llompart francesc andreu (vocal)