Construcción de programas que manejan dinámicamente la memoria
View/ Open
Date
2015-08-06Author
Cherini, Renato
Advisor
Blanco, Javier Oscar, dir.
Metadata
Show full item recordAbstract
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.
Collections
The following license files are associated with this item: