Resumen
La creciente complejidad de los sistemas software ha conducido al desarrollo de metodologias 
formales para la verificaci´on y la correcci´on de datos y programas. Generalmente,
establecer si un programa se comporta seg´un las intenciones originales
del programador o controlar la consistencia y la correcci´on de grandes conjuntos de
datos no son tareas triviales, como atestiguan los numerosos casos de estudio que
encontramos en la bibliograf´ia.
En esta tesis, abordamos dos problemas abiertos de verificaci´on y correcci´on. En
concreto, la verificaci´on y correcci´on de programas declarativos y la verificaci´on y
correcci´on de sitios Web (es decir, conjuntos de datos semiestructurados).
En primer lugar, se ha definido un esquema general para la correcci´on autom´atica
de programas declarativos basados en reglas, que explota una combinaci´on de t´ecnicas
de aprendizaje inductivo top-down y bottom-up. Nuestra metodolog´ia h´ibrida es capaz
de inferir correcciones que son arduas, o incluso imposibles, de conseguir con
un sistema m´as simple de aprendizaje autom´atico puramente top-down o bottom-up.
Adem´as se ha particularizado el esquema general a dos paradigmas de programaci´on
declarativa bien conocidos: el paradigma l´ogico funcional y el paradigma funcional.
En segundo lugar, se ha formalizado un marco para la verificaci´on autom´atica de
sitios Web, que se puede usar para especificar condiciones de integridad sobre ellos,
y luego comprobar autom´aticamente si estas condiciones se satisfacen. Por un lado,
hemos definido un lenguaje de especificaci´on basado en reglas, que permite definir
propiedades tanto sint´acticas como sem´anticas de un sitio Web. Por otro lado, se ha
formalizado una t´ecnica de verificaci´on que detecta patrones incorrectos/prohibidos
y carencia de informaci´on, es decir p`aginas Web incompletas o ausentes. Durante
el proceso de verificaci´on, se recoge informaci´on ´util, que puede ser usada para la
reparaci´on del portal. Por lo tanto, despu´es de la fase de verificaci´on, tambi´en es
posible inferir algunas posibles correcciones para arreglar de manera semi-autom´atica
el sitioWeb err´oneo. Nuestra metodolog´ia se fundamenta en una nueva t´ecnica basada
en reescritura (partial rewriting), en la cual se remplaza el tradicional mecanismo de
pattern matching con una t´ecnica de ajuste m´as conveniente (tree simulation) que
facilita el reconocimiento de patrones en un documento semiestructurado.