En esta tesis se propone una metodología para la certificación de programas Java que está basada en la lógica de reescritura, 
un marco formal lógico y semántico muy general, implementado eficientemente en el lenguaje de programación funcional Maude. 
Se consideran propiedades de seguridad (safety), es decir, propiedades de un sistema que son definidas en términos de que 
no ocurran ciertos eventos. 
 Dichas propiedades se caracterizan como problemas de inalcanzabilidad en la lógica de reescritura. 
Las propiedades de seguridad (safety) se expresan en el estilo de JML, un lenguaje estándar de especificación de módulos Java. 
Con el fin de obtener un procedimiento de decisión utilizamos modelos con un número finito de estados que obtenemos mediante 
el uso de la interpretación abstracta. Partiendo de una  especificación de la semántica de Java escrita en Maude, 
se desarrolla una semántica operacional abstracta con un número finito de estados, también escrita en Maude, que resulta apropiada 
para la verificación de programas. 
Como subproducto de la verificación se entrega un certificado de seguridad, que consiste en  un conjunto de demostraciones 
 basadas en reescritura, que pueden ser comprobadas fácilmente por el consumidor del código mediante el uso de un motor de reescritura estándar. 
La técnica   de código portador de demostración (proof-carrying code) basada en abstracción, denominada JavaPCC, 
ha sido implementada y probada con éxito en varios ejemplos, lo cual demuestra la viabilidad de nuestro enfoque. 

Se analizan propiedades locales de métodos Java, es decir propiedades de sus parámetros y resultados. 
También se analizan propiedades globales de clases Java completas, primero estudiando la no interferencia y luego, el borrado, 
con y sin no interferencia. 
La no interferencia es una propiedad semántica de los programas, que asigna niveles de confidencialidad a los datos y 
evita que haya flujos ilícitos de información desde los niveles de seguridad altos hacia los niveles bajos. 
En esta tesis presentamos un  modelo novedoso de seguridad para la no interferencia global que aproxima la no interferencia como 
una propiedad de seguridad (safety). 
El borrado (de información confidencial) es una forma de reforzar la confidencialidad mediante el aumento de los niveles de confidencialidad
 de los datos, que puede llegar incluso a requerir la eliminación de los datos secretos del sistema. 
En esta tesis, presentamos también un modelo de seguridad para programas Java completos que incluye políticas de no interferencia y borrado.