Resumen de técnicas para el análisis automático de software descrito en lenguajes de programación
David Sanan Baena 
La verificación de modelos o MODEL CHECKING es un método formal que explora de forma exhaustiva el espacio de estados del modelo de un sistema, especificado en alguna técnica de descripción formal, para comprobar la corrección de éste respecto a una serie de propiedades como puede ser análisis de alcanzabilidad, ausencia de interbloqueos, o verificación de propiedades temporales, La verificación de propiedades de un programa escrito en un lenguaje de programación determinado requería la creación manual de un modelo, descrito en la técnica de descripción formal utilizada por la herramienta de análisis. De un tiempo a esta parte han surgido herramientas que realizan la verificación del código de forma automática sin necesidad de realizar manualmente la obtención del modelo. No obstante, la verificación de sistemas de software directamente desde el código fuente lleva consigo una serie de problemas como pueden ser la llamadas externas al lenguaje, la gestión de memoria dinámica o la verificación de propiedades en las estructuras de datos presentes en el programa. En esta tesis detallamos una metodología para la verificación automática de sistemas descritos en lenguajes de programación que hacen uso de APIS bien definidos y de memoria dinámica. Dentro de la verificación de funciones externas nuestra metodología se basa en proporcionar un formalismo del comportamiento de las funciones del API usado por el sistema. De esta forma, se puede verificar la corrección de éste respecto a ese API bien definido. Respecto al uso de la memoria dinámica, en esta tesis proporcionamos un modelo de memoria basado en la división del espacio en dos áreas diferenciadas: el heap y el store global y una lógica de dos niveles, temporal y espacial para la verificación de propiedades sobre estructuras de datos dinámicas. Además, proporcionamos la implementación de estas metodología en dos sistemas muy conocidos en el campo de la verificación: SPIN y CADP.
