CATÁLOGO DE LA BIBLIOTECA DE LA FaMAF
Normal view MARC view ISBD view

Construcción de programas que manejan dinámicamente la memoria / Renato Cherini.

By: Cherini, Renato, 1981-.
Contributor(s): Blanco, Javier Oscar, 1968- [dir.].
Material type: materialTypeLabelBookPublisher: [S.l. : s.n. ], 2015Description: vii, 208 p. : il. ; 30 cm.Subject(s): 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érpretesOnline resources: Acceso a Versión Digital | Acceso a RDU_UNC Disponible en línea.
Partial contents:
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.
Dissertation note: Tesis (Doctor en Cs. de la Computación)--Universidad Nacional de Córdoba, Facultad de Matemática, Astronomía y Física, 2015. Summary: 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.
Tags from this library: No tags from this library for this title. Log in to add tags.
Item type Current location Call number URL Copy number Status Notes Date due Barcode Item holds
Tesis de Doctorado Tesis de Doctorado FaMAF
Vitrina
T C CHE http://www.famaf.unc.edu.ar/institucional/biblioteca/trabajos/639/17301.pdf 1 Available Disponible también en línea 22352
Total holds: 0

Bajo Licencia Creative Commons Atribución-NoComercial-CompartirIgual 2.5 Argentina.

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.

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.

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.

Disponible en línea.

La biblioteca posee 1 ej.

Defensa : 6 de agosto de 2015.

Click on an image to view it in the image viewer

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

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

publicofamaf@gmail.com



//