|
Descripción
|
|
|---|---|
| Existe un gran numero de tecnicas avanzadas de verificacion y optimizacion estatica de programas que han demostrado ser extremadamente utiles en la deteccion de errores de programacion y en la mejora de la eficiencia, y que tienen como factor comun la necesidad de informacion precisa de analisis global del programa. La interpretacion abstracta es una de las tecnicas de analisis mas establecidas, lo que ha permitido el desarrollo de metodos innovadores para la verificacion de programas. Por otra parte, uno de los desafios mas importantes en la investigacion informatica actual consiste en mejorar la capacidad de detectar automaticamente errores en programas y asegurar que un programa es correcto respecto a una determinada especificacion, con el objetivo de producir software fiable. Por ello, la verificacion de programas es un area importante de investigacion, y por ello proporcionar tecnicas avanzadas para detectar errores y verificar sistemas en programas reales complejos es una de las areas mas relevantes en la industria informatica actual. Un enfoque interesante de la verificacion de programas es la denominada verificacion abstracta, una tecnica que tiene como objetivo la verificacion de un programa mediante sobre-aproximaciones de la semantica concreta del programa. Sin embargo, estos metodos no son directamente aplicables a programas reales, pues tecnicas avanzadas como las mencionadas estan en muchos casos disponibles como prototipos, y los avances conseguidos hasta ahora en esta direccion solamente han permitido su aplicacion de modo restringido. El objetivo de esta Tesis Doctoral es desarrollar tecnicas de analisis y verificacion 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 practica de las tecnicas 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. | |
|
Internacional
|
Si |
|
ISBN
|
|
|
Tipo de Tesis
|
Doctoral |
|
Calificación
|
Sobresaliente cum laude |
|
Fecha
|
|