Título: Detección estática de canales no cerrados usando tipos comportamentales

Director: Hernan Melgratti

Jurados: Carlos Lopez Pombo, Christian Roldán

Resumen:

Go es un lenguaje de programación tipado estáticamente cuyo diseño presenta primitivas explícitas de intercambio de mensajes a través de canales. Lange, Ng, Toninho y Yoshida proponen un sistema de tipos comportamentales para analizar propiedades sobre aspectos comunicacionales de programas en Go, tales como ausencia de deadlocks y errores de comunicación. Esta verificación se realiza a través de dos herramientas, Dingo Hunter y Gong, que toman un programa en Go e indican si satisfacen estas propiedades. Furman extiende estas herramientas agregando mensajes de error que contienen información sobre la línea de código que viola las propiedades, y la historia de ejecución asociada. El objetivo de este trabajo es mejorar la usabilidad de las herramientas incorporando una detección estática de canales abiertos, de manera de agregar en el output información sobre canales que no son cerrados y que no se utilizan en el futuro de la ejecución. Para ello se extiende la implementación de Gong de manera de obtener información sobre tipos asociados a canales que se eliminan cuando se construye la máquina de estados que representa la ejecución simbólica de los tipos comportamentales de un programa.