Observatorio de I+D+i UPM

Memorias de investigación
Tesis:
Analysis and Verification of Modular Programs
Año:2008
Áreas de investigación
  • Lenguaje de programación
Datos
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
Esta actividad pertenece a memorias de investigación
Participantes
  • Participante: Jesús Correas (Universidad Complutense de Madrid)
  • Director: Manuel de Hermenegildo Salinas (UPM)
Grupos de investigación, Departamentos, Centros e Institutos de I+D+i relacionados
  • Creador: Grupo de Investigación: Computación lógica, Lenguajes, Implementación y Paralelismo (CLIP)
  • Departamento: Inteligencia Artificial
S2i 2023 Observatorio de investigación @ UPM con la colaboración del Consejo Social UPM
Cofinanciación del MINECO en el marco del Programa INNCIDE 2011 (OTR-2011-0236)
Cofinanciación del MINECO en el marco del Programa INNPACTO (IPT-020000-2010-22)