Construcción de programas que manejan dinámicamente la memoria
Ver/Descargar
Fecha
2015-08-06Autor
Cherini, Renato
Director/a
Blanco, Javier Oscar, dir.
Metadatos
Mostrar el registro completo del ítemResumen
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.
Colecciones
El ítem tiene asociados los siguientes ficheros de licencia: