Construcción de programas que manejan dinámicamente la memoria
Cherini, Renato
1981-
creator
Blanco, Javier Oscar
1968-
dir.
text
ag_
S.l
s.n. ]
2015
monographic
spa
vii, 208 p. : il. ; 30 cm.
En este trabajo abordamos diferentes aspectos de la verificación de programas que manejan dinámicamente la memoria, y más en general, al razonamiento formal sobre ellos. Por un lado, proponemos un marco conceptual para considerar cuestiones ontológicas y epistemológicas de la propia tarea de verificación formal, a través de una generalización del concepto de intérprete, que nos permite relacionar los aspectos abstractos y concretos de la computación. En el plano metodológico, la principal contribución es la introducción
de la Sharing Logic, que permite especificar de forma precisa estructuras dinámicas complejas y las relaciones entre ellas, de manera compatible con los principios de abstracción e information hiding. En el plano práctico, abordamos la decidibilidad del problema de validez de un fragmento de nuestra Sharing Logic que permite caracterizar estructuras de datos como listas enlazadas y segmentos de ellas. Además presentamos un análisis estático, que verifica automáticamente programas que manipulan estructuras de datos no lineales.
Verificación formal -- Lógicas a la Hoare y memoria dinámica -- Automatización y decidibilidad -- Intérpretes -- Funciones de interpretación y sistemas computacionales -- La verificación formal de programas -- El pancomputacionalismo -- Separation logics -- Cálculo de fórmulas -- Especificaciones y razonamiento sobre programas -- Estructuras de datos -- Sharing Logic -- Fórmulas con specified sharing -- Sistema deductivo y reglas de frame -- Tipos abstractos de datos con sharing -- Decidibilidad de la Sharing Logic -- Automatización de Separation Logic -- Analizando grafos generales -- Resultados experimentales.
Renato Cherini.
Incluye apéndices de cada uno de los 6 capítulos.
Tesis (Doctor en Cs. de la Computación)--Universidad Nacional de Córdoba, Facultad de Matemática, Astronomía y Física, 2015.
Bibliografía: p. 195-208.
Disponible en línea.
cc Creative Commons Atribución-NoComercial-CompartirIgual 2.5 Argentina. CC BY-NC-SA https://creativecommons.org/licenses/by-nc-sa/2.5/ar/
Software Engineering
Program verification
Logics and meanings of programs
Artificial Intelligence
Computation by Abstract Devices
Ingeniería de Software
Verificación de programas
Lógica y significado de programas
Inteligencia artificial
Separation logic
Verificación
Memoria dinámica
Análisis estático
Intérpretes
http://hdl.handle.net/11086/2879
http://hdl.handle.net/11086/2879
Creative Commons Atribución-NoComercial-CompartirIgual 2.5 Argentina.
AR_CdUFM
150922
20200427200651.0