Análisis de datos de periódicos digitales

En este proyecto se ha desarrollado una aplicación Web cuya finalidad es ofrecer al usuario datos provenientes del análisis de texto de las noticias que se encuentran en periódicos online. La aplicación permite al usuario realizar búsquedas personalizadas sobre temáticas específicas y configurar algunos tipos de análisis sobre la información recuperada. Entre los análisis que son llevados a cabo destaca el análisis del sentimiento. Para ello se ofrece la posibilidad de que el usuario utilice sus propios diccionarios de pares palabra-valor, utilizados para realizar este tipo de análisis. Para la codificación de la herramienta, se ha utilizado el lenguaje de programación Python y la framework web Django. El almacenamiento de la información de la aplicación se ha realizado sobre una base de datos NoSQL de tipo MongoDB.

Verificación de algoritmos y estructuras de datos en Dafny

La verificación formal de un programa es la demostración de que este funciona de acuerdo a una descripción del comportamiento esperado en toda posible ejecución. La especificación de lo deseado puede utilizar técnicas diversas y entrar en mayor o menor detalle, pero para ganarse el título de formal esta ha de ser matemáticamente rigurosa. El estudio y ejercicio manual de alguna de esas técnicas forma parte del currículo común a los estudios de grado de la Facultad de Informática y del itinerario de Ciencias de la Computación de la Facultad de Ciencias Matemáticas de la Universidad Complutense de Madrid, como es el caso de la verificación con pre- y postcondiciones o lógica de Hoare. En el presente trabajo se explora la automatización de estos métodos mediante el lenguaje y verificador Dafny, con el que se especifican y verifican algoritmos y estructuras de datos de diversa complejidad. Dafny es un lenguaje de programación diseñado para integrar la especificación y permitir la verificación automática de sus programas, con la ayuda del programador y de un demostrador de teoremas en la sombra. Dafny es un proyecto en desarrollo activo aunque suficientemente maduro, que genera programas ejecutables.