Doctorado

Tesis       Trabajos de fin de máster      Cursos de posgrado


Tesis doctorales

Título: Más sobre equivalencias lógicas y distancias entre procesos
Autor: David Romero Hernández
Directores: David de Frutos Escrig
Facultad: Facultad de Informática (Universidad Complutense de Madrid)
Fecha: Febrero 2016
Calificación: Sobresaliente cum Laude

Título: Verificación de extensiones de Redes de Petri con precios, tiempo y múltiples instancias
Autor: María Rosa Martos Salgado
Directores: Fernando Rosa Velardo
Facultad: Facultad de Informática (Universidad Complutense de Madrid)
Fecha: Enero 2016
Calificación: Sobresaliente cum Laude

Título: Sobre la equivalencia entre semánticas operacionales y denotacionales para lenguajes funcionales paralelos
Autor: Lidia Sánchez Gil
Directores: Yolanda Ortega Mallén y Mercedes Hidalgo Herrero
Facultad: Facultad de Informática (Universidad Complutense de Madrid)
Fecha: Julio 2015
Calificación: Sobresaliente cum Laude

Título: Desarrollo dirigido por modelos de aplicaciones seguras para el manejo de información
Autor: Miguel Ángel García de Dios
Directores: Manuel García Clavel
Facultad: Facultad de Informática (Universidad Complutense de Madrid)
Fecha: Abril 2015
Calificación: Sobresaliente cum Laude

Título: Técnicas coalgebraicas y categóricas para el estudio de las semánticas de procesos
Autor: Ignacio Fábregas Alfaro
Directores: David de Frutos Escrig y Miguel Palomino Tarjuelo
Facultad: Facultad de Informática (Universidad Complutense de Madrid)
Fecha: Marzo 2012
Calificación: Sobresaliente cum Laude

Título: Certificación formal de programas en un lenguaje funcional impaciente
Autor: Javier de Dios Castro
Director: Ricardo Peña Marí
Facultad: Facultad de Informática (Universidad Complutense de Madrid)
Fecha: Enero 2012
Calificación: Sobresaliente cum Laude

Título: Análisis de propiedades de seguridad y consumo acotado de memoria en un lenguaje funcional sin recolección de basura
Autor: Manuel Montenegro Montes
Directores: Ricardo Peña Marí y Clara Segura Díaz
Facultad: Facultad de Informática (Universidad Complutense de Madrid)
Fecha: Noviembre 2011
Calificación: Sobresaliente cum Laude

Título: Depuración declarativa y verificación heterogénea en Maude
Autor: Adrián Riesco Rodríguez
Directores: Alberto Verdejo López y Narciso Martí Oliet
Facultad: Facultad de Informática (Universidad Complutense de Madrid)
Fecha: Julio 2011
Calificación: Sobresaliente cum Laude

Título: Análisis de características en el modelo BST
Autor: José Ramón Sánchez Couso
Director: María Inés Fernández Camacho
Facultad: Facultad de Ciencias Matemáticas (Universidad Complutense de Madrid)
Fecha: Abril 2009
Calificación: Sobresaliente cum Laude

Título: An executable formal semantics for OCL with Applications to Formal Analysis and Validation
Autor: Marina Soledad Egea González
Director: Manuel García Clavel
Facultad: Facultad de Informática (Universidad Complutense de Madrid)
Fecha: Noviembre 2008
Calificación: Sobresaliente cum Laude

Título: Redes de Petri móviles para la especificación y verificación de propiedades de seguridad en sistemas ubicuos
Autor: Fernando Rosa Verlardo
Director: David de Frutos Escrig
Facultad: Ciencias Matemáticas (Universidad Complutense de Madrid)
Fecha: Noviembre 2007
Calificación: Sobresaliente cum Laude

Título: Reflexión, abstracción y simulación en la lógica de reescritura
Autor: Miguel Palomino Tarjuelo
Director: Narciso Martí Oliet y José Meseguer
Facultad: Ciencias Matemáticas (Universidad Complutense de Madrid)
Fecha: Marzo 2005
Calificación: Sobresaliente cum Laude

Título: Semánticas formales para un lenguaje funcional paralelo
Autor: Mercedes Hidalgo Herrero
Director: Yolanda Ortega Mallén
Facultad: Ciencias Matemáticas (Universidad Complutense de Madrid)
Fecha: Junio 2004
Calificación: Sobresaliente cum Laude

Título: Técnicas de especificación formal de sistemas orientados a objetos basadas en lógica de reescritura
Autor: Isabel Pita Andreu
Director: Narciso Martí Oliet
Facultad: Ciencias Matemáticas (Universidad Complutense de Madrid)
Fecha: Marzo 2003
Calificación: Sobresaliente cum Laude

Título: Maude como marco semántico ejecutable
Autor: José Alberto Verdejo López
Director: Narciso Martí Oliet
Facultad: Informática (Universidad Complutense de Madrid)
Fecha: Marzo 2003
Calificación: Sobresaliente cum Laude

Trabajos de fin de máster y de doctorado dirigidos

Título: Model Checking TLR* Guarantee Formulas on Infinite Systems
Autor: Óscar Martín Sánchez
Directores: Narciso Martí y Alberto Verdejo
Facultad: Facultad de Informática, Universidad Complutense de Madrid
Fecha: 2013
Calificación: Sobresaliente

Título: Conditional Narrowing Modulo in Rewriting Logic and Maude
Autor: Luis Manuel Aguirre García
Directores: Narciso Martí, Miguel Palomino e Isabel Pita
Facultad: Facultad de Informática, Universidad Complutense de Madrid
Fecha: 2013
Calificación: Matrícula de honor

Título: Especificación y análisis del protocolo Chord en Maude
Autor: Sara Manchado
Directores: Isabel Pita y Alberto Verdejo
Facultad: Facultad de Informática, Universidad Complutense de Madrid
Fecha: 2012
Calificación: Notable

Título: Two Algorithms for Model Checking of Regular Linear Temporal Logic
Autor: Julián Samborski-Forlese
Directores: Miguel Palomino y César Sánchez
Facultad: Facultad de Informática, Universidad Complutense de Madrid
Fecha: 2012
Calificación: Notable

Título: Developing Secure Business Applications from Secure BPMN Models
Autor: Javier Valdazo
Directores: Manuel Clavel
Facultad: Facultad de Informática, Universidad Complutense de Madrid
Fecha: 2012
Calificación: Aprobado

Título: MySQL4OCL: Un compilador de OCL a MySQL
Autor: Carolina Dania
Directores: Manuel Clavel y Marina Egea
Facultad: Facultad de Informática, Universidad Complutense de Madrid
Fecha: 2011
Calificación: Sobresaliente

Título: Decision Procedures for the Temporal Verification of Concurrent Data Structures
Autor: Alejandro Sánchez
Director: Miguel Palomino y César Sánchez
Facultad: Facultad de Informática, Universidad Complutense de Madrid
Fecha: 2011
Calificación: Sobresaliente

Título: Avances recientes en análisis estáticos de terminación
Autor: Agustín Delgado Muñoz
Director: Ricardo Peña Marí
Facultad: Facultad de Informática, Universidad Complutense de Madrid
Fecha: 2010
Calificación: Notable

Título: Evaluación de métricas de calidad del software sobre un programa Java
Autor: Ana María García Sánchez
Director: Manuel Clavel
Facultad: Facultad de Informática, Universidad Complutense de Madrid
Fecha: 2010
Calificación: Notable

Título: Towards verifying Petri nets: a model checking approach
Autor: María Rosa Martos-Salgado
Director: Fernando Rosa y David de Frutos Escrig
Facultad: Facultad de Informática, Universidad Complutense de Madrid
Fecha: 2010
Calificación: Sobresaliente

Título: Caracterizaciones lógicas uniformes de las semánticas de procesos
Autor: David Romero-Hernández
Director: David de Frutos Escrig
Facultad: Facultad de Informática, Universidad Complutense de Madrid
Fecha: 2010
Calificación: Sobresaliente

Título: Introducción a la notación BPMN y su relación con las estrategias del lenguaje Maude
Autor: Laura Henche Grande
Director: Narciso Martí Oliet
Facultad: Facultad de Informática, Universidad Complutense de Madrid
Fecha: 2009
Calificación: Notable

Título: Aplicando las estrategias de Maude
Alumno: Javier Palencia
Director: Narciso Martí y Alberto Verdejo
Facultad: Ciencias Matemáticas (Universidad Complutense de Madrid)
Fecha: 2008
Calificación: Notable

Título: Sobre la equivalencia entre semánticas operacionales y denotacionales para lenguajes funcionales paralelos
Autor: Lidia Sánchez Gil
Director: Yolanda Ortega Mallén
Facultad: Ciencias Matemáticas (Universidad Complutense de Madrid)
Fecha: 2008
Calificación: Sobresaliente

Título: Inferencia de tipos seguros en un lenguaje funcional con destrucción explícita de memoria
Autor: Manuel Montenegro Montes
Director: Ricardo Peña Marí y Clara María Segura Díaz
Departamento: Sistemas Informáticos y Computación
Facultad: Facultad de Informática (Universidad Complutense de Madrid)
Fecha: 21 de Septiembre de 2007
Calificación: Sobresaliente

Título: Distributed and mobile applications in Maude
Autor: Adrián Riesco Rodríguez
Director: José Alberto Verdejo López
Departamento: Sistemas Informáticos y Computación
Facultad: Facultad de Informática (Universidad Complutense de Madrid)
Fecha: 1 de Junio de 2007
Calificación: Sobresaliente

Título: Un estudio coalgebraico de las simulaciones
Autor: Ignacio Fábregas Alfaro
Director: David de Frutos Escrig y Miguel Palomino Tarjuelo
Departamento: Sistemas Informáticos y Programación
Facultad: Facultad de Matemáticas (Universidad Complutense de Madrid)
Fecha: Septiembre 2006
Calificación: Sobresaliente

Título: A Formal Tool for the Specification and Analysis of Software Architectures
Autor: Alexandre Rademaker
Director: Christiano de Oliveira Braga
Facultad: Universidade Federal Fluminense
Fecha: Mayo 2005

Título: An Implementation of Modular Structural Operational Semantics in Maude
Autor: Fabricio Chalub
Director: Christiano de Oliveira Braga
Facultad: Universidade Federal Fluminense
Fecha: Mayo 2005

Título: ITP/ASIP: A verification tool for imperative programs base don algebraic semantics
Autor: Juan López Santa Cruz
Director: Manuel García Clavel
Departamento: Sistemas Informáticos y Programación
Facultad: Informática (Universidad Complutense de Madrid)
Fecha: Septiembre 2005
Calificación: Sobresaliente

Título: ITP/OCL: A theorem prover-based tool for UML+OCL class diagrams
Autor: Marina Egea González
Director: Manuel García Clavel y Narciso Martí Oliet
Departamento: Sistemas Informáticos y Programación
Facultad: Informática (Universidad Complutense de Madrid)
Fecha: Septiembre 2005
Calificación: Sobresaliente

Título: Typing Techniques for Security in Mobile Agent Systems
Autor: Fernando Rosa Velardo
Director: David de Frutos Escrig
Departamento: Sistemas Informáticos y Programación
Facultad: Facultad de Matemáticas (Universidad Complutense de Madrid)
Fecha: Junio 2004
Calificación: Sobresaliente

Título: Aplicaciones de la Programación Funcional Paralela al Álgebra
Autor: Rafael Martínez Torres
Director: Ricardo Peña Marí
Departamento: Sistemas Informáticos y Programación
Facultad: Informática (Universidad Complutense de Madrid)
Fecha: Junio 2004
Calificación: Sobresaliente

Título: Lógicas ambientales: propiedades, aplicaciones y técnicas de comprobación de modelos
Autor: José Miguel Cleva Millor
Director: David de Frutos Escrig y Yolanda Ortega Mallén
Departamento: Sistemas Informáticos y Programación
Facultad: Ciencias Matemáticas (Universidad Complutense de Madrid)
Fecha: Septiembre 2003
Calificación: Sobresaliente

Historial docente en programas de posgrado

Curso académico: 2011-2012

Título del curso: Especificación y validación de software
Profesores participantes: Manuel García Clavel, Narciso Martí Oliet, Miguel Palomino Tarjuelo y José Alberto Verdejo López

Título del curso: Modelos de sistemas concurrentes y distribuidos
Profesores participantes: Yolanda Ortega Mallén y David de Frutos Escrig

Título del curso: Análisis y transformación de programas
Profesores participantes: Elvira Albert Albiol, Ricardo Peña Marí y Clara María Segura Díaz

Título del curso: Modelado de Sólidos y Técnicas de Visualización
Profesores participantes: Antonio Gavilanes Franco, Pedro J. Martín de la Calle y José Alberto Verdejo López

Curso académico: 2010-2011

Título del curso: Especificación y validación de software
Profesores participantes: Francisco Durán, Manuel García Clavel, Narciso Martí Oliet y Miguel Palomino Tarjuelo

Título del curso: Modelos de sistemas concurrentes y distribuidos
Profesores participantes: Yolanda Ortega Mallén y David de Frutos Escrig

Título del curso: Análisis y transformación de programas
Profesores participantes: Elvira Albert Albiol y Clara María Segura Díaz

Título del curso: Modelado de Sólidos y Técnicas de Visualización
Profesores participantes: Antonio Gavilanes Franco, Pedro J. Martín de la Calle y José Alberto Verdejo López

Curso académico: 2009-2010

Título del curso: Especificación y validación de software
Profesores participantes: Manuel García Clavel, Narciso Martí Oliet, Miguel Palomino Tarjuelo y José Alberto Verdejo López

Título del curso: Modelos de sistemas concurrentes y distribuidos
Profesores participantes: Yolanda Ortega Mallén, María Inés Fernández Camacho y David de Frutos Escrig

Título del curso: Análisis y transformación de programas
Profesores participantes: Elvira Albert Albiol, Ricardo Peña Marí y Clara María Segura Díaz

Título del curso: Modelado de Sólidos y Técnicas de Visualización
Profesores participantes: Antonio Gavilanes Franco, Pedro J. Martín de la Calle y José Alberto Verdejo López

Curso académico: 2008-2009

Título del curso: Especificación y validación de software
Profesores participantes: Manuel García Clavel, Narciso Martí Oliet, Miguel Palomino Tarjuelo y José Alberto Verdejo López

Título del curso: Modelos de sistemas concurrentes y distribuidos
Profesores participantes: David de Frutos Escrig y Luis LLana Díaz

Título del curso: Análisis y transformación de programas
Profesores participantes: Elvira Albert Albiol, Ricardo Peña Marí y Clara María Segura Díaz

Curso académico: 2007-2008

Título del curso: Especificación y validación de software
Profesores participantes: Manuel García Clavel, Narciso Martí Oliet, Isabel Pita Andreu y José Alberto Verdejo López

Título del curso: Modelos de sistemas concurrentes y distribuidos
Profesores participantes: David de Frutos Escrig, Olga Marroquin Alonso

Título del curso: Análisis y transformación de programas de programas
Profesores participantes: Elvira Albert Albiol, Purificación Arenas Sánchez, Cristóbal Pareja Flores, Ricardo Peña Marí, Germán Puebla (UPM) y Clara María Segura Díaz

Curso académico: 2006-2007

Título del curso: Especificación y validación de software
Profesores participantes: Manuel García Clavel, Narciso Martí Oliet, Isabel Pita Andreu y José Alberto Verdejo López

Título del curso: Modelos de sistemas concurrentes y distribuidos
Profesores participantes: David de Frutos Escrig, María Inés Fernández Camacho y Luis Llana Díaz

Título del curso: Análisis y transformación de programas de programas
Profesores participantes: Elvira Albert Albiol, Cristóbal Pareja Flores, Ricardo Peña Marí, Germán Puebla (UPM) y Clara María Segura Díaz

Curso académico: 2005-2006

Título del curso: Especificación y validación de software
Profesores participantes: Manuel García Clavel, Narciso Martí Oliet, Isabel Pita Andreu y José Alberto Verdejo López

Título del curso: Modelos de sistemas concurrentes y distribuidos
Profesores participantes: David de Frutos Escrig, María Inés Fernández Camacho y Yolanda Ortega Mallén

Título del curso: Análisis y transformación de programas de programas
Profesores participantes: Elvira Albert Albiol, Cristóbal Pareja Flores, Ricardo Peña Marí, Germán Puebla (UPM) y Clara María Segura Díaz

Curso académico: 2004-2005

Título del curso: Especificación y validación de software
Profesores participantes: Manuel García Clavel, Narciso Martí Oliet, Isabel Pita Andreu y José Alberto Verdejo López

Título del curso: Modelos de sistemas concurrentes y distribuidos
Profesores participantes: David de Frutos Escrig, Margarita Bradley Delso, María Inés Fernández Camacho, Luis Llana Díaz y Yolanda Ortega Mallén

Título del curso: Técnicas de análisis de programas y su aplicación a la compilación
Profesores participantes: Elvira Albert Albiol, Cristóbal Pareja Flores, Ricardo Peña Marí, Germán Puebla (UPM) y Clara María Segura Díaz

Curso académico: 2003-2004

Título del curso: Modelos formales de la concurrencia
Profesores participantes: David de Frutos Escrig, María Inés Fernández Camacho, Luis Llana Díaz, Natalia López Barquilla

Título del curso: Especificación y verificación de sistemas en lógica de reescritura
Profesores participantes: Manuel García Clavel, Narciso Martí Oliet, Yolanda Ortega Mallén, Isabel Pita Andreu, José Alberto Verdejo López

Título del curso: Técnicas de análisis de programas y su aplicación a la compilación
Profesores participantes: Ricardo Peña Marí, Clara María Segura Díaz

Curso académico: 2002-2003

Título del curso: Desarrollo formal de sistemas basados en agentes móviles
Profesores participantes: David de Frutos Escrig, María Inés Fernández Camacho, Luis Llana Díaz, Manuel Núñez García, Yolanda Ortega Mallén, Fernando Rubio Diez

Título del curso: Técnicas de análisis de programas y su aplicación a la compilación
Profesores participantes: Ricardo Peña Marí, Clara María Segura Díaz