Analizando la forma de estructuras de datos no lineales en memoria dinámica con Separation Logic

Abstract

Presentamos un shape analysis con garantı́as de terminación para programas que manipulan estructuras de datos no lineales como árboles binarios. El análisis se basa en una ejecución simbólica de los programas sobre estados abstractos compuestos por fórmulas de un conjunto restringido de la Separation Logic. Dada una precondición, calcula automáticamente una postcondición e invariantes concisos para los ciclos del programa. El uso de un nivel de relevancia para las variables según el tipo de manipulación que sufren permite lograr un balance entre precisión y abstracción en las fórmulas. Mostramos los resultados obtenidos por un prototipo que implementa nuestro análisis sobre una variedad de ejemplos.

We present a terminating shape analysis for programs manipulating non- linear data structures such as binary trees. The analysis is based on symbolic execution of programs over abstract states composed by formulæ of a restricted subset of Separation Logic. Given a precondition, it automatically calculates concise postconditions and invariants for program loops. The use of relevan- ce level of program variables depending on the manipulations applied on them gives us a balance between precision and abstraction in the formulæ. We re- port experimental results obtained from running a prototype implementing our analysis on a variety of examples.