Analizando la forma de estructuras de datos no lineales en memoria dinámica con Separation Logic
Date
2017-05-31Author
Rearte, Lucas Agustín
Advisor
Cherini, Renato, dir.
Blanco, Javier Oscar, dir.
Metadata
Show full item recordAbstract
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.