Imagen de cubierta local
Imagen de cubierta local
Imagen de Google Jackets

Analizando la forma de estructuras de datos no lineales en memoria dinámica con Separation Logic / Lucas Agustín Rearte.

Por: Colaborador(es): Detalles de publicación: [S.l. : s.n. ], 2017.Descripción: 73 p. : il. ; 30 cmTema(s): Recursos en línea: Nota de disertación: 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. Resumen: 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.Resumen: We present a terminating shape analysis for programs manipulating nonlinear 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 relevance level of program variables depending on the manipulations applied on them gives us a balance between precision and abstraction in the formulæ. We report experimental results obtained from running a prototype implementing our analysis on a variety of examples.
Etiquetas de esta biblioteca: No hay etiquetas de esta biblioteca para este título.
Existencias
Tipo de ítem Biblioteca actual Signatura URL Copia número Estado Notas Fecha de vencimiento Código de barras Reserva de ítems
Trabajo Especial de Grado Trabajo Especial de Grado FaMAF Secc. Tesis y Trabajos especiales Trabajo Especial Computación CAJA 21 - 22955 Enlace al Recurso 1 Disponible Disponible también en línea 22955
Total de reservas: 0

Bajo Licencia Creative Commons Atribución CompartirIgual 2.5 Argentina.

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.

Bibliografía: p. 71-73.

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 nonlinear 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 relevance level of program variables depending on the manipulations applied on them gives us a balance between precision and abstraction in the formulæ. We report experimental results obtained from running a prototype implementing our analysis on a variety of examples.

Haga clic en una imagen para verla en el visor de imágenes

Imagen de cubierta local


Nuestras Redes Sociales

facebook Instagram

Horario de la Biblioteca: lunes a viernes de 8:30 a 18:30hs

Av. Medina Allende s/n , Ciudad Universitaria, Córdoba, Argentina

Tel: +54 351 5353701 int. 41127 (Atención al Público) int. 41151 (Dirección)

biblio@famaf.unc.edu.ar (Dirección)

publicofamaf@gmail.com (Atención al público)