Catálogo de publicaciones

Dada una descripción formal de los estados válidos del heap -por ejemplo, un invariante de una estructuras de datos- las cotas ajustadas para los campos del heap son el conjunto de los valores que pueden tomar los campos en alguna instancia válida. Así, los valores de campos que no pertenecen a las cotas ajustadas pueden ser ignorados por los análisis automáticos (acotados) de código, reduciendo así el espacio de estados a explorar, y mejorando la performance del análisis. Sin embargo, el cómputo de cotas ajustadas es costoso. El único enfoque conocido que computa estas cotas en un tiempo aceptable, TACO+, es intrínsecamente paralelo, y requiere de un cluster con varias computadoras para su ejecución eficiente. En este trabajo se aborda el problema de computar eficientemente cotas ajustadas en entornos de ejecución secuenciales. Así, se presentan dos nuevos enfoques para resolver este problema. El primero, denominado bottom-up, utiliza un procedimiento de decisión basado en SAT para visitar instancias válidas del heap, y computa cotas ajustadas usando los valores de los campos de estas instancias. bottom-up, al igual que TACO+, requiere de una especificación en algún lenguaje declarativo de alto nivel -como JML para JAVA- de los estados válidos del heap. De esta manera, bottom-up y TACO+ generan cotas ajustadas equivalentes. El segundo, SLBD, se basa en una especificación del heap en términos de un predicado inductivo de la lógica de separación. Este enfoque computa cotas ajustadas mientras realiza (un número finito de) desplegados del predicado inductivo de entrada. En algunos casos SLBD puede producir cotas ajustadas diferentes a las de TACO+ (y bottom-up). Se evaluaron experimentalmente los enfoques bottom-up, SLBD y la técnica relacionada TACO+, en la generación de cotas ajustadas para varias clases contenedoras JAVA. Los resultados muestran que, en un ambiente de ejecución secuencial, bottom-up es un orden de magnitud más rápido que TACO+ (secuencializado), y que SLBD es dos órdenes de magnitud más rápido que bottom-up. Además, se evaluó el impacto de las cotas ajustadas generadas por nuestros enfoques en la veri ficación de código y en la generación exhaustiva de estructuras (que satisfacen un predicado) basados en SAT. Los resultados indican que los enfoques que computan cotas ajustadas secuencialmente (vía bottom-up o SLBD), y luego las aprovechan durante el análisis, son significativamente más eficientes que los análisis convencionales, que no explotan la idea de cotas ajustadas. Además, para los análisis basados en SAT mencionados, los resultados muestran que las cotas ajustadas computadas por SLBD tienen un impacto similar a las computadas por TACO+ y bottom-up.

Tesis de Maestría