Analizando la forma de estructuras de datos no lineales en memoria dinámica con Separation Logic
Tesis (Lic. en Ciencias de la Computación)--Universidad Nacional de Córdoba, Facultad de Matemática, Astronomía, Física y Computación, 2017.
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | bachelorThesis |
| Language: | spa |
| Published: |
2018
|
| Subjects: | |
| Online Access: | http://hdl.handle.net/11086/5838 |
| _version_ | 1801215663104065536 |
|---|---|
| author | Rearte, Lucas Agustín |
| author2 | Cherini, Renato, dir. |
| author_facet | Cherini, Renato, dir. Rearte, Lucas Agustín |
| author_sort | Rearte, Lucas Agustín |
| collection | Repositorio Digital Universitario |
| description | Tesis (Lic. en Ciencias de la Computación)--Universidad Nacional de Córdoba, Facultad de Matemática, Astronomía, Física y Computación, 2017. |
| format | bachelorThesis |
| id | rdu-unc.5838 |
| institution | Universidad Nacional de Cordoba |
| language | spa |
| publishDate | 2018 |
| record_format | dspace |
| spelling | rdu-unc.58382022-10-13T11:33:32Z Analizando la forma de estructuras de datos no lineales en memoria dinámica con Separation Logic Rearte, Lucas Agustín Cherini, Renato, dir. Blanco, Javier Oscar, dir. Teoría de la computación Theory of Computation Memoria dinámica Arboles binarios Program reasoning Separation logic Program verification Shape analysis Memory leak Tesis (Lic. en Ciencias de la Computación)--Universidad Nacional de Córdoba, Facultad de Matemática, Astronomía, Física y Computación, 2017. 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. 2018-02-19T13:33:01Z 2018-02-19T13:33:01Z 2017-05-31 bachelorThesis http://hdl.handle.net/11086/5838 spa Atribución-CompartirIgual 2.5 Argentina https://creativecommons.org/licenses/by-sa/2.5/ar/ |
| spellingShingle | Teoría de la computación Theory of Computation Memoria dinámica Arboles binarios Program reasoning Separation logic Program verification Shape analysis Memory leak Rearte, Lucas Agustín Analizando la forma de estructuras de datos no lineales en memoria dinámica con Separation Logic |
| title | Analizando la forma de estructuras de datos no lineales en memoria dinámica con Separation Logic |
| title_full | Analizando la forma de estructuras de datos no lineales en memoria dinámica con Separation Logic |
| title_fullStr | Analizando la forma de estructuras de datos no lineales en memoria dinámica con Separation Logic |
| title_full_unstemmed | Analizando la forma de estructuras de datos no lineales en memoria dinámica con Separation Logic |
| title_short | Analizando la forma de estructuras de datos no lineales en memoria dinámica con Separation Logic |
| title_sort | analizando la forma de estructuras de datos no lineales en memoria dinamica con separation logic |
| topic | Teoría de la computación Theory of Computation Memoria dinámica Arboles binarios Program reasoning Separation logic Program verification Shape analysis Memory leak |
| url | http://hdl.handle.net/11086/5838 |
| work_keys_str_mv | AT reartelucasagustin analizandolaformadeestructurasdedatosnolinealesenmemoriadinamicaconseparationlogic |