En esta tesi es proposa una metodologia per a la certificació de programes Java que està basada en la lògica de reescriptura, 
un marc formal lògic i semàntic molt general, implementat eficientment en el llenguatge de programació funcional Maude. 
 Es consideren propietats de seguretat (safety), ès a dir, propietats d'un sistema que són definides en termes de
 certs esdeveniments que no han d'ocórrer. Eixes propietats es caracteritzen com a problemes d'inassolibilitat  
 en la lògica de reescriptura. 
 Les propietats de seguretat (safety) s'expressen en l'estil de JML, un llenguatge estàndard d'especificació de mòduls Java.
 A fi d'obtindre un procediment de decisió utilitzem models amb un número finit d'estats que obtenim per mitjà de l'ús de 
la interpretació abstracta.
 Partint d'una especificació de la semàntica de Java escrita en Maude, es desenvolupa una semàntica operacional abstracta
 amb un número finit d'estats, també escrita en Maude, que resulta apropiada per a la verificació de programes.
 Com a subproducte de la verificació s'entrega un certificat de seguretat, que consistix d'un conjunt de demostracions 
 basades en reescriptura, que poden ser comprovades fàcilment pel consumidor del codi per mitjà de l'ús d'un motor de 
reescriptura estàndard.
 La tècnica de codi portador de demostració (proof-carrying code) basada en abstracció, denominada JavaPCC, 
ha sigut implementada i provada amb èxit en diversos exemples, la qual cosa demostra la viabilitat del nostre enfocament. 

 S'analitzen propietats locals de mètodes Java, és a dir, propietats dels seus paràmetres i resultats. 
També s'analitzen propietats globals de classes Java completes, primer estudiant la no interferència i després, l'esborrament, 
amb i sense no interferència.
 La no interferència és una propietat semàntica dels programes, que assigna nivells de confidencialitat a les dades 
i evita que hi haja fluxos il.lícits d'informació des dels nivells de seguretat alts cap als nivells baixos.
 En esta tesi presentem un model nou de seguretat per a la no interferència global que aproxima la no interferència 
com una propietat d'innocuïtat (safety).
 L'esborrament (d'informació confidencial) ès una forma de reforçar la confidencialitat per mitjà de l'augment en els nivells 
de confidencialitat de les dades, que pot arribar inclús a requerir l'eliminació de les dades secretes del sistema.
 En esta tesi, presentem també un model de seguretat per a programes Java complets que inclou polítiques de no interferència i esborrament.