Mejorando la aplicación de abstracción por predicados a especificaciones DynAlloy

Abstract

En este trabajo presentamos técnicas para mejorar la performance de Abstracción por Predicados en el contexto de análisis de especificaciones DynAlloy. Este trabajo extiende nuestro trabajo previo en la misma dirección, principalmente mediante un mecanismo de detección de inducción, que permite independizar, bajo ciertas condiciones, el tiempo de análisis del programa de la cota en la cantidad de iteraciones exigida por DynAlloy. Dado que el tiempo de análisis de programas DynAlloy depende exponencialmente de dicha cota, las ganancias obtenidas al aplicar esta optimizaci´on son notables. Sin embargo, la técnica no es aplicable en casos arbitrarios, sino sólo bajo ciertas condiciones que identificamos en este trabajo. Por otra parte, la técnica puede requerir intervención del usuario, a través de la introducción manual de predicados de abstracción. Las optimizaciones mencionadas fueron incorporadas a la implementación de nuestra herramienta, permiténdonos evaluar las mismas en diversos casos de estudio que reportamos en este artículo. Estos casos de estudio corresponden a modelos DynAlloy provenientes de programas que operan sobre listas enlazadas.