Láminas de la sesión

by user








Láminas de la sesión
Mensaje de Tesis
Hilo conductor
Raúl Monroy
Mensaje de tesis
• Strunk, W. Elements of Style, Bartleby. 1918
13. Make the paragraph the unit of composition
Qué es
• Resumen de tesis:
– En el que cada frase, idealmente, corresponde a
un capítulo de la tesis, delineando el objetivo del
– Que declara el argumento central de la tesis (el
objeto del comunicado)
Para qué sirve
• Asegurar la articulación y covertura de la tesis
• Coordinar la organización de todos los textos producidos
durante el doctorado
• Responder al qué he hecho y al por qué esto merece un
• Determinar el contenido y el objetivo de cada capítulo
• Habilitar el desarrollo top – down, bottom – up de la tesis
• Habilitar el desarrollo independiente de cada capítulo.
The Computational Modelling of Religious
by Fr. Aloysius Hacker
• We apply ideas from Computer Science to the understanding of
religious concepts.
• Previous attempts to explain religious concepts,
– e.g. the holy trinity and miracles.
have often encountered philosophical problems.
• These problems arose because the appropriate terminology was
not available.
– Computational terminology often provides an appropriate analogy.
• Although some problems still remain,
– e.g. free will,
• We are seeing the beginning of a new, computational theology.
Planning Proofs of Correctness of CCS Systems
by Raúl Monroy
1. The specification and verification of communicating systems have
captured increasing interest, because they are error prone.
2. CCS was especially designed to help this enterprise, and is widely
used in both industry and academia.
3. Existing methods to automate the use of CCS to verification have
centred around finite-state systems, using bisimulations.
4. This, though, is insufficient to deal with systems that contain
infinite states or a finite, but arbitrary, number of components,
VIPS; there is an alternative approach, based on fixed point
equations, which does not exhibit such limitations; however,
automated verification in this context is extremely difficult.
5. This thesis investigates the use of explicit proof plans for
automating the verification of VIPS.
6. We have extended inductive proof planning, with special
plans that exploit both the inductive structure and
7. the expected behaviour of a system during its verification.
8. With these plans, we have developed a fully automated
verification method, which has been successfully tested
on a number of examples that are outside the domain of
other, rival techniques.
9. Therefore, even though it has still got plenty of room for
10. Our techniqe successfully automates the equational
approach to verification of CCS systems.
Towards Building a Masquerade Detection
Masquerade detection has been actively studied for more than a decade,
especially after the seminal work of Schonlau’s group
Schonlau suggested that, to profile a user, one should model the history of the
commands she would enter into a UNIX session; he developed a masquerade
dataset, SEA, which has been the standard for comparing masquerade detection
However, the performance of SEA-based methods is not conclusive, and, as a
result, research on masquerade detection has resorted to other sources of
information for profiling user behaviour.
We claim that to better characterise user behaviour, it is necessary to consider
how and what the user browses while working on her own file system.
To capture this behaviour, we introduce a navigation structure, which contains
information about the use (visit) of file system objects, and about the structure
of the user file system; we have used the navigation structure to build a oneclass classifier for masquerade detection.
While preliminary, our results are encouraging and suggest a number of ways in
which new methods can be constructed.
• El mensaje de tesis comunica un argumento
central, articulado y completo
• Puede aplicarse para la especificación de
libros, capítulos, secciones
– Privilegiando la redacción orientada a párrafos
• Agiliza la escritura y estructuración de
documentos, permitiendo el desarrollo
independiente de secciones, bajo un modelo
top–down y bottom–up
• Desarrolla el mensaje de tu tesis
• Compleméntalo con una especificación más
detallada de cada capítulo, ejemplo:
– “Chapter 1 introduces the general notion of computer
modelling and how it might be applied to religion by
drawing analogies between computational concepts
and religious ones to suggest consequences and nonconsequences of religious positions, and hence debug
some of the theological debate of the last two
• Fecha de entrega: próxima sesión
Fly UP