Alpuente Frasnedo, MaríaAlba Castro, Mauricio Fernando2011-10-202011-10-202008-072011-10-20https://riunet.upv.es/handle/10251/12247En esta tesis se presenta una metodología y la implementación correspondiente para la certificación de propiedades de seguridad de programas Java, basada en lógica de reescritura, semántica de lenguajes de programación e interpretación abstracta. Se consideran propiedades aritméticas basadas en tipos, no interferencia y consumo acotado de recursos.164Reserva de todos los derechosLógica de reescrituraVerificaciónCódigo portador de prueba (PCC)Interpretación abstractaLENGUAJES Y SISTEMAS INFORMATICOSMáster Universitario en Ingeniería del Software, Métodos Formales y Sistemas de Información-Màster Universitari en Enginyeria del Programari, Mètodes Formals i Sistemes D'InformacióTesis de másterAbierto