Análisis estático de programas

Abstract

En el presente trabajo se describen las líneas de investigación en desarrollo por el grupo de investigación en análisis estático de propiedades de programas. Los integrantes del grupo atacan el problema del análisis de propiedades de programas mediante diferentes enfoques. Algunos trabajan a nivel de modelos mientras que otros lo hacen directamente a nivel de código fuente. Se utilizan técnicas tanto de análisis estático liviano como pesados (basados en demostradores de teoremas o model-checking). En una línea de trabajo se investiga en análisis estático de propiedades de programas a nivel de código fuente, usando diferentes técnicas como métodos livianos basados en interpretación abstracta y lógicas especí cas como separation logic. Otra línea realiza análisis de propiedades de seguridad en programas en formatos de bajo nivel (bytecode) utilizando sistemas de tipos desarrollados a medida. La última línea de trabajo se basa en el análisis de propiedades de modelos de procesos de negocios usando métodos formales.