Alumno: Daniel Romero
Titulo Thesis: Rewriting-based Verification  and  Debugging of Web Systems

Resumen

El incremento de la complejidad de los sistemas Web ha dado lugar al desarrollo de sofisticadas metodologías formales para verificar y corregir la información y los programas en la Web.
En general, establecer si un sistema Web se comporta correctamente con respecto a la intención original del programador así como verificar su consistencia no son tareas triviales.
La prueba de esto es la cantidad de estudios al respecto que existen en la literatura.

En esta tesis abordamos dos problemas interesantes relacionados a la verificación de sistemas Web.

En primer lugar, extendemos un marco previo de verificación Web, basado en reescritura parcial, agregando una técnica para la reparación de sistemas Web.
Proponemos una metodología de reparación básica que está dotada con distintas estrategias para obtimizar el número de acciones que deben ser ejecutadas para reparar un sitio Web dado.
Además, desarrollamos una mejora del marco de verificación Web que está basada en interpretación abstracta y  mejora en gran medida la eficiencia y la escalabilidad de la técnica original.

En segundo lugar, formalizamos un marco lógico de reescritura para la especificación y model-chequeo de aplicaciones Web dinámicas.
Nuestro marco nos permite simular la navegación de un usuario y evaluar los scripts Web dentro de la aplicación Web, así como verificar importantes propiedades tales como alcanzabilidad y 
consistencia.
Cuando una propiedad es refutada, es entregado un contra ejemplo con la traza errónea.
Esta información puede ser analizada con el fin de depurar la aplicación Web que se está examinando.
Para este propósito, formulamos una novedosa técnica de slicing hacia atrás sobre las trazas. 
Esta técnica consiste en rastrear hacia atrás, sobre la traza de ejecución, los símbolos relevantes del término (o estado) que estamos interesado en observar.