Construcción de programas que manejan dinámicamente la memoria
Tesis (Doctor en Cs. de la Computación)--Universidad Nacional de Córdoba, Facultad de Matemática, Astronomía y Física, 2015.
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | doctoralThesis |
| Language: | spa |
| Published: |
2016
|
| Subjects: | |
| Online Access: | http://hdl.handle.net/11086/2879 |
| _version_ | 1801212003659808768 |
|---|---|
| author | Cherini, Renato |
| author2 | Blanco, Javier Oscar, dir. |
| author_facet | Blanco, Javier Oscar, dir. Cherini, Renato |
| author_sort | Cherini, Renato |
| collection | Repositorio Digital Universitario |
| description | Tesis (Doctor en Cs. de la Computación)--Universidad Nacional de Córdoba, Facultad de Matemática, Astronomía y Física, 2015. |
| format | doctoralThesis |
| id | rdu-unc.2879 |
| institution | Universidad Nacional de Cordoba |
| language | spa |
| publishDate | 2016 |
| record_format | dspace |
| spelling | rdu-unc.28792022-10-13T11:16:22Z Construcción de programas que manejan dinámicamente la memoria Cherini, Renato Blanco, Javier Oscar, dir. Ingeniería de Software Lógica y significado de programas Inteligencia artificial Software Engineering Logics and meanings of programs Artificial Intelligence Verificación Memoria dinámica Análisis estático Tesis (Doctor en Cs. de la Computación)--Universidad Nacional de Córdoba, Facultad de Matemática, Astronomía y Física, 2015. 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. 2016-08-04T16:23:13Z 2016-08-04T16:23:13Z 2015-08-06 doctoralThesis http://hdl.handle.net/11086/2879 spa Atribución-NoComercial-CompartirIgual 2.5 Argentina http://creativecommons.org/licenses/by-nc-sa/2.5/ar/ |
| spellingShingle | Ingeniería de Software Lógica y significado de programas Inteligencia artificial Software Engineering Logics and meanings of programs Artificial Intelligence Verificación Memoria dinámica Análisis estático Cherini, Renato Construcción de programas que manejan dinámicamente la memoria |
| title | Construcción de programas que manejan dinámicamente la memoria |
| title_full | Construcción de programas que manejan dinámicamente la memoria |
| title_fullStr | Construcción de programas que manejan dinámicamente la memoria |
| title_full_unstemmed | Construcción de programas que manejan dinámicamente la memoria |
| title_short | Construcción de programas que manejan dinámicamente la memoria |
| title_sort | construccion de programas que manejan dinamicamente la memoria |
| topic | Ingeniería de Software Lógica y significado de programas Inteligencia artificial Software Engineering Logics and meanings of programs Artificial Intelligence Verificación Memoria dinámica Análisis estático |
| url | http://hdl.handle.net/11086/2879 |
| work_keys_str_mv | AT cherinirenato construcciondeprogramasquemanejandinamicamentelamemoria |